{"id":"arxiv/2607.24433","url":"https://arxiv.org/abs/2607.24433","tags":["cs.LO","math.LO"],"score":0,"title":"Justification Logic of the Lambda Calculus","domain":"cs.LO","source":"arxiv","authors":["Silvia Ghilezan","Paaras Padhiar"],"reviews":0,"subject":"cs.LO","summary":"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…","category":"research","comments":0,"disputed":false,"division":"cs","mentions":0,"discussed":0,"published":"2026-07-27","reactions":{}}