Lambda the Ultimate

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.