# Strongly Normalizing Audited Computation

## TL;DR

This paper introduces a new, simpler calculus for auditing in programming languages, ensuring strong normalization and consistency, thus providing a solid logical foundation for secure and accountable computation.

## Contribution

The authors present $oldsymbol{ extlambda^{hc}}$, a simpler, consistent, and strongly normalizing calculus for auditing based on Justification Logic, improving upon previous complex systems.

## Key findings

- $oldsymbol{ extlambda^{hc}}$ is simpler than $oldsymbol{ extlambda^h}$.
- $oldsymbol{ extlambda^{hc}}$ is proven to be strongly normalizing.
- The proof of strong normalization is formalized in Nominal Isabelle.

## Abstract

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.