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.
@InProceedings{ricciotti_et_al:LIPIcs.CSL.2017.36, author = {Ricciotti, Wilmer and Cheney, James}, title = {{Strongly Normalizing Audited Computation}}, booktitle = {26th EACSL Annual Conference on Computer Science Logic (CSL 2017)}, pages = {36:1--36:21}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-045-3}, ISSN = {1868-8969}, year = {2017}, volume = {82}, editor = {Goranko, Valentin and Dam, Mads}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2017.36}, URN = {urn:nbn:de:0030-drops-76817}, doi = {10.4230/LIPIcs.CSL.2017.36}, annote = {Keywords: lambda calculus, justification logic, strong normalization, audited computation} }
Feedback for Dagstuhl Publishing