Justification Logic of the Lambda Calculus
2026-07-27 • Logic in Computer Science
Logic in Computer Science
AI summaryⓘ
The authors explore a logic system where computer programs and logical proofs are treated as the same thing through a connection called the Curry-Howard correspondence. They create a new logic that uses the exact typed lambda calculus programs as proofs within the logic, allowing reasoning about computation and proof together. They provide formal rules, a natural deduction system, and a sequent calculus with important properties like cut-elimination to ensure consistent reasoning and simplification of proofs. This work bridges computation and logic in a more direct and formal way than previous approaches.
simply typed lambda calculusintuitionistic propositional logicCurry-Howard correspondencejustification logicmodal logicnatural deductionsequent calculuscut-eliminationnormalisation
Authors
Silvia Ghilezan, Paaras Padhiar
Abstract
The simply typed λ-calculus is a model of computation where typed terms correspond to proofs of intuitionistic propositional logic (IPL) via the Curry-Howard correspondence. Justification logic is an operational modal logic in which the standard box modality is replaced by an explicit proof term, allowing the logic itself to reason directly about proofs of its formulas. Standard justification logics reason about proofs of IPL by embedding Hilbert-style axiomatic proofs of IPL as proof terms of the logic. We instead introduce a justification logic of the λ-calculus, in which the proof terms of the modality are exactly the typed λ-terms themselves: a modal logic that reasons about computation and proof simultaneously, as both notions coincide under the Curry-Howard interpretation. First, we provide an axiomatisation of this logic. We then propose a natural deduction system and a Curry-Howard interpretation, where a formal connection between the term calculus and the proof terms of the logic is provided. To complete the picture, we give a Gentzen-style sequent calculus for which we prove cut-elimination, and consequently obtain a normalisation result by working in the negative fragment.