Implementation of Proof Search in the Imperative Programming Language Pizza

  • Christian Urban
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1397)


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.


Success Continuations G4ip Pizza 


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. [Car84]
    M. Carlsson. On Implementing Prolog in Functional Programming. New Generation Computing, pages 347–359, 1984.Google Scholar
  2. [Dyc92]
    R. Dyckhoff. Contraction-Free Sequent Calculi for Intuitionistic Logic. Journal of Symbolic Logic, 57(3):795–807, September 1992.zbMATHCrossRefMathSciNetGoogle Scholar
  3. [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
  4. [HM94]
    J. Hodas and D. Miller. Logic Programming in a Fragment of Intuitionistic Linear Logic. Information and Computation, 110(2):327–365, 1994.zbMATHCrossRefMathSciNetGoogle Scholar
  5. [MNPS91]
    D. Miller, G. Nadathur, F. Pfenning, and A. Scedrov. Uniform Proofs as a Foundation for Logic Programming. Annals of Pure Applied Logic, 51:125–157, 1991.CrossRefzbMATHMathSciNetGoogle Scholar
  6. [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
  7. [TS96]
    A. S. Troelstra and H. Schwichtenberg. Basic Proof Theory. Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 1996.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1998

Authors and Affiliations

  • Christian Urban
    • 1
  1. 1.Computer LaboratoryUniversity of Cambridge, Gonville and Caius CollegeCambridgeUK

Personalised recommendations