Explicit Auditing

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

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

Publication series

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

Conference

Conference15th International Colloquium on Theoretical Aspects of Computing
Abbreviated titleICTAC 2018
Country/TerritorySouth Africa
CityStellenbosch
Period12/10/1819/10/18
Internet address

Keywords

  • cs.LO
  • cs.PL
  • 68N18

Fingerprint

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

Cite this