2026-07-25T01:21:52Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:7681 2024-03-06T10:40:47Z ddc:004 open_access

Strongly Normalizing Audited Computation Ricciotti, Wilmer Cheney, James lambda calculus justification logic strong normalization audited computation 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^hc, consistent, and strongly normalizing. Our proof of strong normalization is formalized in Nominal Isabelle. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Wilmer Ricciotti and James Cheney 2017 Is Part Of LIPIcs, Volume 82, 26th EACSL Annual Conference on Computer Science Logic (CSL 2017) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.CSL.2017.36 urn:nbn:de:0030-drops-76817 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2017.36 eng https://creativecommons.org/licenses/by/3.0/legalcode