TWAM: a certifying abstract machine for logic programs

DOI10.1007/978-3-030-03592-1_7zbMATH Open1403.68035arXiv1801.00471OpenAlexW2963825363MaRDI QIDQ1629962FDOQ1629962

Authors: Brandon Bohrer, Karl Crary 

Publication date: 7 December 2018

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.

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

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

Mathematics Subject Classification ID

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

Cites Work

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

Cited In (3)

• Title not available (Why is that?)
• TWAM: a certifying abstract machine for logic programs
• Title not available (Why is that?)

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)