TWAM: a certifying abstract machine for logic programs

DOI10.1007/978-3-030-03592-1_7zbMath1403.68035arXiv1801.00471OpenAlexW2963825363MaRDI QIDQ1629962

Karl Crary, Brandon Bohrer

Publication date: 7 December 2018

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

Mathematics Subject Classification ID

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

Related Items (1)

TWAM: a certifying abstract machine for logic programs

Cites Work

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

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