The correctness of a higher-order lazy functional language implementation: An exercise in mechanical theorem proving
DOI10.1007/3-540-61254-8_24zbMATH Open1407.68091OpenAlexW1492125303MaRDI QIDQ4645809FDOQ4645809
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
Recommendations
- scientific article; zbMATH DE number 2040977
- scientific article
- 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
Grammars and rewriting systems (68Q42) Functional programming and lambda calculus (68N18) Semantics in the theory of computing (68Q55)
Cites Work
- Isabelle. A generic theorem prover
- Title not available (Why is that?)
- Comprehending monads
- Two-Level Functional Languages
- Implementing lazy functional languages on stock hardware: the Spineless Tagless G-machine
- Deriving a lazy abstract machine
- Computational adequacy via ‘mixed’ inductive definitions
- Title not available (Why is that?)
- The congruence of two programming language definitions
- Title not available (Why is that?)
- Title not available (Why is that?)
Cited In (4)
Uses Software
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)
