Home » forums » LtU Forum

The Logic of Proofs

In another thread Paul Snively mentions the Logic of Proofs with references to several papers.

The Basic Intuitionistic Logic of Proofs (PDF), Explicit Provability and Constructive Semantics (PS) are two. The third is probably the one most immediately relevant/applicable to LtU.

Reflective lambda-calculus (PS) by Jesse Alt and Sergei Artemov. 2001.

We introduce a general purpose typed λ-calculus λ∞ which contains intuitionistic logic, is capable of internalizing its own derivations as λ-terms and yet enjoys strong normalization with respect to a natural reduction system. In particular, λ∞ subsumes the typed λ-calculus. The Curry-Howard isomorphism converting intuitionistic proofs into λ∞terms is a simple instance of the internalization property of λ∞. The standard semantics of λ∞ is given by a proof system with proof checking capacities. The system λ∞ is a theoretical prototype of reflective extensions of a broad class of type-based systems in programming languages, provers, AI and knowledge representation, etc.

By Derek Elkins at 2008-01-20 21:39 | LtU Forum | previous forum topic | next forum topic | other blogs | 1198 reads

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

Actually...

You may want to take another look at the Basic Intuitionistic Logic of Proofs paper, as it builds on the Reflective lambda-calculus paper and, being intuitionistic, might suggest ways in which the logic could be embedded, e.g. in Coq. In other words, it might not take that much to make iLP the framework for a type system used in a new programming language with a certified compiler developed in Coq (or a similar tool).

By Paul Snively at Tue, 2008-01-22 06:47 | login or register to post comments