TWAM: A Certifying Abstract Machine for Logic Programs

TL;DR

This paper introduces TWAM, a certifying abstract machine with a dependent type system for logic programs, enabling correctness guarantees through type-preserving compilation from T-Prolog.

Contribution

It presents the design and implementation of TWAM, a new certifying abstract machine with a dependent type system for logic programming, and a soundness theorem ensuring correctness.

Findings

TWAM can specify logic program semantics within LF.

The compiler from T-Prolog to TWAM is certifying and correct.

A soundness theorem guarantees partial correctness of well-typed programs.

Abstract

Type-preserving (or typed) compilation uses typing derivations to certify correctness properties of compilation. We have designed and implemented a type-preserving compiler for a simply-typed dialect of Prolog we call T-Prolog. The crux of our approach is a new certifying abstract machine which we call the Typed Warren Abstract Machine (TWAM). The TWAM has a dependent type system strong enough to specify the semantics of a logic program in the logical framework LF. We present a soundness metatheorem which constitutes a partial correctness guarantee: well-typed programs implement the logic program specified by their type. This metatheorem justifies our design and implementation of a certifying compiler from T-Prolog to TWAM.