A verified prolog compiler for the Warren Abstract Machine

DOI10.1016/0743-1066(92)90054-7MaRDI QIDQ4015948zbMATH OpenOpenAlexWikidataFDO

Authors David M. Russinoff

Publication date 10 November 1992

Published in The Journal of Logic Programming (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/0743-1066(92)90054-7

zbMATH Keywords

compilationPrologWarren Abstract Machine

Mathematics Subject Classification ID

Logic programming (68N17) Theory of compilers and interpreters (68N20) Specification and verification (program logics, model checking, etc.) (68Q60) Artificial intelligence (68T99)

Recommendations

• scientific article; zbMATH DE number 4094776
• Automated verification of Prolog programs
• scientific article; zbMATH DE number 3956408
• scientific article; zbMATH DE number 868104
• scientific article; zbMATH DE number 4176425
• The WAM case study: Verifying compiler correctness for Prolog with KIV
• scientific article; zbMATH DE number 1223558
• An improved proof-theoretic compilation of logic programs
• scientific article; zbMATH DE number 7453192

Cited in

(25)

• C-expressions: A variable-free calculus for equational logic programming
• Specification, verification and prototyping of an optimized compiler
• TWAM: a certifying abstract machine for logic programs
• Specification and correctness proof of a WAM extension with abstract type constraints
• How to invent a Prolog machine
• The WAM case study: Verifying compiler correctness for Prolog with KIV
• scientific article; zbMATH DE number 4176425 (Why is no real title available?)
• scientific article; zbMATH DE number 4178749 (Why is no real title available?)
• Skolem Machines and Geometric Logic
• Towards Description and Optimization of Abstract Machines in an Extension of Prolog
• Some global optimizations for a PROLOG compiler
• scientific article; zbMATH DE number 3986672 (Why is no real title available?)
• scientific article; zbMATH DE number 408786 (Why is no real title available?)
• scientific article; zbMATH DE number 512904 (Why is no real title available?)
• Run-time type computations in the Warren Abstract machine
• Partial translation: towards a portable and efficient prolog implementation technology
• scientific article; zbMATH DE number 1950443 (Why is no real title available?)
• scientific article; zbMATH DE number 1543041 (Why is no real title available?)
• Description and optimization of abstract machines in a dialect of Prolog
• Global Optimizations in a Prolog Compiler for the Toam
• scientific article; zbMATH DE number 773979 (Why is no real title available?)
• An improved proof-theoretic compilation of logic programs
• Lightweight compilation of (C)LP to JavaScript
• Towards a methodology for the design of abstract machines for logic programming languages
• Verification of compiler correctness for the WAM

This page was built for publication: A verified prolog compiler for the Warren Abstract Machine

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