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 |
| Keywords: | |
| 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. |
| Download: | POSTSCRIPT COPY |
![[Search These Pages]](http://www.dai.ed.ac.uk/icons/dai_search.gif){kind=icon}
![[DAI Home Page]](http://www.dai.ed.ac.uk/icons/dai_home.gif){kind=icon}
![[Comment]](http://www.dai.ed.ac.uk/icons/dai_comment.gif){kind=icon}