Theorem proving and program synthesis with Oyster

Christian Horn, Alan Smaill

Research output: Book/ReportBook


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.
Original languageEnglish
PublisherUniversity of Edinburgh, Department of Artificial Intelligence
Number of pages12
Publication statusPublished - 1990

Fingerprint Dive into the research topics of 'Theorem proving and program synthesis with Oyster'. Together they form a unique fingerprint.

Cite this