TY - GEN
T1 - Justification logic and history based computation
AU - Bavera, Francisco
AU - Bonelli, Eduardo
PY - 2010
Y1 - 2010
N2 - Justification Logic (JL) is a refinement of modal logic that has recently been proposed for explaining well-known paradoxes arising in the formalization of Epistemic Logic. Assertions of knowledge and belief are accompanied by justifications: the formula [[t]]A states that t is "reason" for knowing/believing A. We study the computational interpretation of JL via the Curry-de Bruijn-Howard isomorphism in which the modality [[t]]A is interpreted as: t 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.
AB - Justification Logic (JL) is a refinement of modal logic that has recently been proposed for explaining well-known paradoxes arising in the formalization of Epistemic Logic. Assertions of knowledge and belief are accompanied by justifications: the formula [[t]]A states that t is "reason" for knowing/believing A. We study the computational interpretation of JL via the Curry-de Bruijn-Howard isomorphism in which the modality [[t]]A is interpreted as: t 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.
UR - http://www.scopus.com/inward/record.url?scp=78049446275&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=78049446275&partnerID=8YFLogxK
U2 - 10.1007/978-3-642-14808-8_23
DO - 10.1007/978-3-642-14808-8_23
M3 - Conference contribution
AN - SCOPUS:78049446275
SN - 3642148077
SN - 9783642148071
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 337
EP - 351
BT - Theoretical Aspects of Computing, ICTAC 2010 - 7th International Colloquium, Proceedings
T2 - 7th International Colloquium on Theoretical Aspects of Computing, ICTAC 2010
Y2 - 1 September 2010 through 3 September 2010
ER -