Justification logic and history based computation. (English) Zbl 1286.03045

Bavera, Francisco; Bonelli, Eduardo

Cavalcanti, Ana (ed.) et al., Theoretical aspects of computing – ICTAC 2010. 7th international colloquium, Natal, Rio Grande do Norte, Brazil, September 1–3, 2010. Proceedings. Berlin: Springer (ISBN 978-3-642-14807-1/pbk). Lecture Notes in Computer Science 6255, 337-351 (2010).

Summary: 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.
For the entire collection see [Zbl 1194.68019].

MSC:

03B42	Logics of knowledge and belief (including belief change)
03B40	Combinatory logic and lambda calculus
68N18	Functional programming and lambda calculus

Software:

AProVE; Automath