LambdaMu-PRL - 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 LambdaMu-PRL that combines the propositional fragment of computational type theory with classical reasoning rules from the LambdaMu-calculi. The calculus supports the top-down 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 mu--safe terms to identify proof terms corresponding to constructive proofs and show that the restriction of LambdaMu-PRL to mu-safe proof terms is sound and complete for intuitionistic propositional logic. We also show that an extension of LambdaMu-PRL to arithmetical and first-order expressions is isomorphic to Murthy's calculus PROG_K.


BACK
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" }