Implementation of Proof Search in the Imperative Programming Language Pizza
- 226 Downloads
Automated proof search can be easily implemented in logic programming languages. We demonstrate the technique of success continuations, which provides an equally simple method for encoding proof search in imperative programming languages. This technique is exemplified by developing an interpreter for the calculus G4ip in the language Pizza.
KeywordsSuccess Continuations G4ip Pizza
Unable to display preview. Download preview PDF.
- [Car84]M. Carlsson. On Implementing Prolog in Functional Programming. New Generation Computing, pages 347–359, 1984.Google Scholar
- [EP91]C. Elliott and F. Pfenning. A Semi-Functional Implementation of a Higher-Order Logic Programming Language. In P. Lee, editor, Topics in Advanced Language Implementation, pages 289–352. MIT Press, 1991.Google Scholar
- [OW97]M. Odersky and P. Wadler. Pizza into Java: Translating Theory into Practice. In Proc. 24th ACM Symposium on Principles of Programming Languages, January 1997.Google Scholar
- [TS96]A. S. Troelstra and H. Schwichtenberg. Basic Proof Theory. Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 1996.Google Scholar