scientific article; zbMATH DE number 2079040

MaRDI QIDQ4474853zbMATH OpenFDO

Authors David R. Lester, Sava Mintchev

Publication date 21 July 2004

zbMATH Keywords

Lambda CalculusDenotational SemanticsTheorem ProverCompiler CorrectnessCongruence Proof

Mathematics Subject Classification ID

Theory of compilers and interpreters (68N20) Combinatory logic and lambda calculus (03B40) Functional programming and lambda calculus (68N18)

Recommendations

• The correctness of a higher-order lazy functional language implementation: An exercise in mechanical theorem proving
• A verified compiler for an impure functional language
• scientific article; zbMATH DE number 3846848
• Proving correctness of a compiler using step-indexed logical relations
• Structure of a Proof-Producing Compiler for a Subset of Higher Order Logic

Cited in

(12)

• A provably correct compilation of functional languages into scripting languages
• The correctness of a higher-order lazy functional language implementation: An exercise in mechanical theorem proving
• Proving correctness of a compiler using step-indexed logical relations
• A certified extension of the Krivine machine for a call-by-name higher-order imperative language
• Pilsner: a compositionally verified compiler for a higher-order imperative language
• Biorthogonality, step-indexing and compiler correctness
• A list-machine benchmark for mechanized metatheory (extended abstract)
• A verified compiler for an impure functional language
• Compilation as Rewriting in Higher Order Logic
• The correctness of a code generator for a functional language
• A list-machine benchmark for mechanized metatheory
• Correctness of procedure representations in higher-order assembly language

Describes a project that uses

Uses Software

• Isabelle

This page was built for publication:

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