Explicit Auditing

TL;DR

This paper introduces an efficient implementation of the Calculus of Audited Units (CAU), a typed lambda calculus with runtime inspection of computation trails, through explicit substitutions and auditing operations, culminating in a call-by-value abstract machine.

Contribution

It presents a novel approach to optimize the untyped variant of CAU using explicit substitutions and auditing, enabling practical execution of trail inspection.

Findings

Developed a call-by-value abstract machine for CAU.

Improved efficiency in reducing terms with audited trails.

Facilitated practical runtime trail inspection in computation.

Abstract

The Calculus of Audited Units (CAU) is a typed lambda calculus resulting from a computational interpretation of Artemov's Justification Logic under the Curry-Howard isomorphism; it extends the simply typed lambda calculus by providing audited types, inhabited by expressions carrying a trail of their past computation history. Unlike most other auditing techniques, CAU allows the inspection of trails at runtime as a first-class operation, with applications in security, debugging, and transparency of scientific computation. An efficient implementation of CAU is challenging: not only do the sizes of trails grow rapidly, but they also need to be normalized after every beta reduction. In this paper, we study how to reduce terms more efficiently in an untyped variant of CAU by means of explicit substitutions and explicit auditing operations, finally deriving a call-by-value abstract machine.