Justification Logic and Audited Computation

FRANCISCO BAVERA; EDUARDO BONELLI

JOURNAL OF LOGIC AND COMPUTATION

OXFORD UNIV PRESS

Lugar: Oxford; Año: 2015

0955-792X

Justification Logic (\JL) is a refinement of modal logic in which assertions of knowledge and belief are accompanied by justifications: the formula $\valid{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 $\valid{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.