A verified prolog compiler for the Warren Abstract Machine

DOI10.1016/0743-1066(92)90054-7zbMath0754.68037OpenAlexW2006804775WikidataQ123182249 ScholiaQ123182249MaRDI QIDQ4015948

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

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

Related Items

TWAM: a certifying abstract machine for logic programs, Specification, verification and prototyping of an optimized compiler, An Improved Proof-Theoretic Compilation of Logic Programs, C-expressions: A variable-free calculus for equational logic programming, Specification and correctness proof of a WAM extension with abstract type constraints