The University of Edinburgh -
Division of Informatics
Forrest Hill & 80 South Bridge

Research Paper #505

Title:Theorem Proving and Program Synthesis with Oyster
Authors:Horn,C; Smaill,AD
Date: 1990
Presented:In Proceedings of the Unified Computation Laboratory, Institute of Mathematics and its Applications, Sttirling, 1990
Abstract:Martin-Loef 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 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.

[Search These Pages] [DAI Home Page] [Comment]