Justification logic and history based computation

Francisco Bavera, Eduardo Bonelli

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

8 Scopus citations

Abstract

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.

Original languageEnglish
Title of host publicationTheoretical Aspects of Computing, ICTAC 2010 - 7th International Colloquium, Proceedings
Pages337-351
Number of pages15
DOIs
StatePublished - 2010
Event7th International Colloquium on Theoretical Aspects of Computing, ICTAC 2010 - Natal, Brazil
Duration: 1 Sep 20103 Sep 2010

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume6255 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference7th International Colloquium on Theoretical Aspects of Computing, ICTAC 2010
Country/TerritoryBrazil
CityNatal
Period1/09/103/09/10

Fingerprint

Dive into the research topics of 'Justification logic and history based computation'. Together they form a unique fingerprint.

Cite this