Justification logic and audited computation

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.