The correctness of a higher-order lazy functional language implementation: An exercise in mechanical theorem proving

DOI10.1007/3-540-61254-8_24zbMath1407.68091OpenAlexW1492125303MaRDI QIDQ4645809

Sava Mintchev, David R. Lester

Publication date: 11 January 2019

Published in: Higher-Order Algebra, Logic, and Term Rewriting (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/3-540-61254-8_24

zbMATH Keywords

abstract machineoperational semanticsdenotational semanticsfunctional languagetheorem prover

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18) Semantics in the theory of computing (68Q55) Grammars and rewriting systems (68Q42)

Uses Software

• Isabelle

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• The congruence of two programming language definitions
• Isabelle. A generic theorem prover
• Implementing lazy functional languages on stock hardware: the Spineless Tagless G-machine
• Two-Level Functional Languages
• Comprehending monads
• Deriving a lazy abstract machine
• Computational adequacy via ‘mixed’ inductive definitions