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.
Recent comments
16 weeks 2 days ago
16 weeks 2 days ago
16 weeks 2 days ago
38 weeks 3 days ago
42 weeks 5 days ago
44 weeks 2 days ago
44 weeks 2 days ago
47 weeks 19 hours ago
51 weeks 5 days ago
51 weeks 5 days ago