Justification Logic and History-Based Computation

FRANCISCO BAVERA; EDUARDO BONELLI

LECTURE NOTES IN COMPUTER SCIENCE

Springer-Verlag

Año: 2010 vol. 6255 p. 337 - 351

0302-9743

Justification Logic (JL) is a refinement of modal logic thathas recently been proposed for explaining well-known paradoxes arisingin the formalization of Epistemic Logic. Assertions of knowledge and beliefare accompanied by justifications: the formula [[t]]A states that t is“reason” for knowing/believing A. We study the computational interpretationof JL via the Curry-de Bruijn-Howard isomorphism in whichthe modality [[t]]A is interpreted as: t is a type derivation justifying thevalidity of A. The resulting lambda calculus is such that its terms areaware of the reduction sequence that gave rise to them. This serves as abasis for understanding systems, many of which belong to the securitydomain, in which computation is history-aware.