Martin Lof type theory provides a formal framework for the construction of verified programs, both specified and written in the type theory. We describe an implementation of the type of theory that aims to provide an environment for software engineering using this approach. We illustrate this by describing the synthesis of a simple evaluator for arithmetic expressions in the system.
|Publisher||University of Edinburgh, Department of Artificial Intelligence|
|Number of pages||12|
|Publication status||Published - 1990|