Strongly Normalizing Audited Computation

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract / Description of output

Auditing is an increasingly important operation for computer programming, for example in security (e.g. to enable history-based access control) and to enable reproducibility and accountability (e.g. provenance in scientific programming). Most proposed auditing techniques are ad hoc or treat auditing as a second-class, extralinguistic operation; logical or semantic foundations for auditing are not yet well-established. Justification Logic (JL) offers one such foundation; Bavera and Bonelli introduced a computational interpretation of JL called $\lambda^h$ that supports auditing. However, $\lambda^h$ is technically complex and strong normalization was only established for special cases. In addition, we show that the equational theory of $\lambda^h$ is inconsistent. We introduce a new calculus $\lambda^{hc}$ that is simpler than $\lambda^h$, consistent, and strongly normalizing. Our proof of strong normalization is formalized in Nominal Isabelle.
Original languageEnglish
Title of host publication26th EACSL Annual Conference on Computer Science Logic (CSL 2017)
PublisherSchloss Dagstuhl - Leibniz-Zentrum fuer Informatik, Germany
Number of pages21
ISBN (Print)978-3-95977-045-3
Publication statusPublished - 24 Aug 2017
Event26th EACSL Annual Conference on Computer Science Logic - Stockholm, Sweden
Duration: 20 Aug 201724 Aug 2017

Publication series

NameLeibniz International Proceedings in Informatics (LIPIcs)
PublisherSchloss Dagstuhl--Leibniz-Zentrum fuer Informatik
ISSN (Print)1868-8969


Conference26th EACSL Annual Conference on Computer Science Logic
Abbreviated titleCSL 2017
Internet address

Keywords / Materials (for Non-textual outputs)

  • cs.LO


Dive into the research topics of 'Strongly Normalizing Audited Computation'. Together they form a unique fingerprint.

Cite this