Verification of compiler correctness for the WAM

DOI10.1007/BFB0105415MaRDI QIDQ6567724zbMATH OpenFDO

Authors Cornelia Pusch

Publication date 5 July 2024

Full work available at URL https://doi.org/10.1007/BFB0105415

Mathematics Subject Classification ID

Logic programming (68N17) Theory of compilers and interpreters (68N20) Semantics in the theory of computing (68Q55) Specification and verification (program logics, model checking, etc.) (68Q60) Formalization of mathematics in connection with theorem provers (68V20)

Recommendations

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

Cites work

• A verified prolog compiler for the Warren Abstract Machine
• Denotational and operational semantics for prolog
• Evolving Algebras 1993: Lipari Guide
• scientific article; zbMATH DE number 43398 (Why is no real title available?)
• scientific article; zbMATH DE number 1142320 (Why is no real title available?)
• Isabelle. A generic theorem prover

Cited in

(1)

• From high to low: simulating nondeterminism and state with state

This page was built for publication: Verification of compiler correctness for the WAM

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