Justification logic and audited computation

Abstract

Justification Logic ( JL ) is a refinement of modal logic in which assertions of knowledge and belief are accompanied by justifications: the formula 〚s〛A states that s is a ‘reason’ for knowing/believing A . We study the computational interpretation of JL via the Curry–Howard isomorphism in which the modality 〚s〛A is interpreted as: s is a type derivation justifying the validity of A . The resulting lambda calculus is such that its terms are aware of the reduction sequence that gave rise to them. This serves as a basis for understanding systems, many of which belong to the security domain, in which computation is history-aware.