TWAM: a certifying abstract machine for logic programs

DOI10.1007/978-3-030-03592-1_7MaRDI QIDQ1629962zbMATH OpenOpenAlexFDO

Authors Brandon Bohrer, Karl Crary

Publication date 7 December 2018

Full work available at URL https://arxiv.org/abs/1801.00471

Mathematics Subject Classification ID

Logic programming (68N17) Theory of compilers and interpreters (68N20)

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.

Recommendations

• scientific article; zbMATH DE number 773979
• The WAM case study: Verifying compiler correctness for Prolog with KIV
• A verified prolog compiler for the Warren Abstract Machine
• scientific article; zbMATH DE number 408786
• scientific article; zbMATH DE number 1543041

Cites work

• scientific article; zbMATH DE number 4180832 (Why is no real title available?)
• scientific article; zbMATH DE number 65531 (Why is no real title available?)
• scientific article; zbMATH DE number 408786 (Why is no real title available?)
• scientific article; zbMATH DE number 1543041 (Why is no real title available?)
• scientific article; zbMATH DE number 773979 (Why is no real title available?)
• A Machine-Oriented Logic Based on the Resolution Principle
• A dependently typed assembly language
• A framework for defining logics
• A verified prolog compiler for the Warren Abstract Machine
• An Efficient Unification Algorithm
• An expressive, scalable type theory for certified code
• CakeML
• Formal certification of a compiler back-end or: programming a compiler with a proof assistant
• Foundational certified code in the Twelf metalogical framework
• Lectures on the Curry-Howard isomorphism
• Proof-producing translation of higher-order logic into pure and stateful ML
• Stack-based typed assembly language
• TWAM: a certifying abstract machine for logic programs
• The Abella Interactive Theorem Prover (System Description)

Cited in

(3)

• TWAM: a certifying abstract machine for logic programs
• scientific article; zbMATH DE number 773979 (Why is no real title available?)
• scientific article; zbMATH DE number 408786 (Why is no real title available?)

This page was built for publication: TWAM: a certifying abstract machine for logic programs

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1629962)