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

DOI10.1007/3-540-61254-8_24MaRDI QIDQ4645809zbMATH OpenOpenAlexFDO

Authors 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

denotational semanticsabstract machineoperational semanticstheorem proverfunctional language

Mathematics Subject Classification ID

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

Recommendations

• scientific article; zbMATH DE number 2040977
• scientific article; zbMATH DE number 5007860
• scientific article; zbMATH DE number 4113956
• Publication:4941901
• The semantics of lazy functional languages
• Inductive prover based on equality saturation for a lazy functional language
• Implementing theorem provers in a purely functional style

Cites work

• scientific article; zbMATH DE number 4179333 (Why is no real title available?)
• scientific article; zbMATH DE number 1231468 (Why is no real title available?)
• scientific article; zbMATH DE number 675533 (Why is no real title available?)
• scientific article; zbMATH DE number 2079040 (Why is no real title available?)
• Comprehending monads
• Computational adequacy via ‘mixed’ inductive definitions
• Deriving a lazy abstract machine
• Implementing lazy functional languages on stock hardware: the Spineless Tagless G-machine
• Isabelle. A generic theorem prover
• The congruence of two programming language definitions
• Two-Level Functional Languages

Cited in

(5)

• scientific article; zbMATH DE number 2086498 (Why is no real title available?)
• The adequacy of Launchbury's natural semantics for lazy evaluation
• scientific article; zbMATH DE number 2079040 (Why is no real title available?)
• A functional correspondence between call-by-need evaluators and lazy abstract machines
• scientific article; zbMATH DE number 5007860 (Why is no real title available?)

Describes a project that uses

Uses Software

• Isabelle

This page was built for publication: The correctness of a higher-order lazy functional language implementation: An exercise in mechanical theorem proving

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