TY - JOUR
T1 - Justification logic and audited computation
AU - Bavera, Francisco
AU - Bonelli, Eduardo
N1 - Publisher Copyright:
© The Author, 2015. Published by Oxford University Press. All rights reserved.
PY - 2018/7/20
Y1 - 2018/7/20
N2 - 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.
AB - 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.
KW - Curry-Howard
KW - History-based computation
KW - Justification Logic
KW - Lambda Calculus
KW - Modal Logic
UR - http://www.scopus.com/inward/record.url?scp=85054526185&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85054526185&partnerID=8YFLogxK
U2 - 10.1093/logcom/exv037
DO - 10.1093/logcom/exv037
M3 - Article
AN - SCOPUS:85054526185
SN - 0955-792X
VL - 28
SP - 909
EP - 934
JO - Journal of Logic and Computation
JF - Journal of Logic and Computation
IS - 5
ER -