LambdaMuPRL  A Proof Refinement
Calculus for Classical Reasoning in Computational Type Theory


Nuria Brede, Christoph Kreitz.  
Technical Report, Universität Potsdam, March 2009. 

Abstract 

We present a hybrid proof calculus LambdaMuPRL that combines the
propositional fragment of computational type theory with classical reasoning
rules from the LambdaMucalculi. The calculus supports the topdown
development of proofs as well as the extraction of proof terms in a functional
programming language extended by a nonconstructive binding operator.
It enables a user to employ a mix of constructive and classical reasoning
techniques and to extract algorithms from proofs of specification theorems
that are fully executable if classical arguments occur only in proof parts
related to the validation of the algorithm.
We prove the calculus sound and complete for classical propositional logic,
introduce the concept of musafe terms to identify proof terms
corresponding to constructive proofs and show that the restriction of
LambdaMuPRL to musafe proof terms is sound and complete for
intuitionistic propositional logic. We also show that an extension of
LambdaMuPRL to arithmetical and firstorder expressions is isomorphic
to Murthy's calculus PROG_K.

Back to overview of papers 

Bibtex Entry 

@TechReport{tr:Allen+02a, author = "Nuria Brede and Christoph Kreitz", title = "$\lambda\mu$PRL  A Proof Refinement Calculus for Classical Reasoning in Computational Type Theory", institution = "Institut f{\"u}r Informatik, Universit{\"a}t Potsdam", year = "2009" } 