Justification logic and audited computation

Francisco Bavera, Eduardo Bonelli

Research output: Contribution to journalArticlepeer-review


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.

Original languageEnglish
Pages (from-to)909-934
Number of pages26
JournalJournal of Logic and Computation
Issue number5
StatePublished - Jul 20 2018

ASJC Scopus subject areas

  • Software
  • Theoretical Computer Science
  • Logic
  • Arts and Humanities (miscellaneous)
  • Hardware and Architecture


  • Curry-Howard
  • History-based computation
  • Justification Logic
  • Lambda Calculus
  • Modal Logic


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

Cite this