Explicit Auditing

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

Abstract / Description of output

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.
Original languageEnglish
Title of host publicationInternational Colloquium on Theoretical Aspects of Computing
EditorsBernd Fischer, Tarmo Uustalu
PublisherSpringer, Cham
Number of pages20
ISBN (Electronic)978-3-030-02508-3
ISBN (Print)978-3-030-02507-6
Publication statusPublished - 15 Oct 2018
Event15th International Colloquium on Theoretical Aspects of Computing - Stellenbosch, South Africa
Duration: 12 Oct 201819 Oct 2018

Publication series

NameLecture Notes in Computer Science
ISSN (Electronic)0302-9743


Conference15th International Colloquium on Theoretical Aspects of Computing
Abbreviated titleICTAC 2018
Country/TerritorySouth Africa
Internet address

Keywords / Materials (for Non-textual outputs)

  • cs.LO
  • cs.PL
  • 68N18


Dive into the research topics of 'Explicit Auditing'. Together they form a unique fingerprint.

Cite this