Formal verifications of call-by-need and call-by-name evaluations with mutual recursion

DOI10.1007/978-3-030-34175-6_10MaRDI QIDQ6536314zbMATH OpenFDO

Authors Masayuki Mizuno, Eijiro Sumii

Publication date 19 April 2024

Full work available at URL https://doi.org/10.1007/978-3-030-34175-6_10

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18) 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

• Formal verification of the correspondence between call-by-need and call-by-name
• Small-step and big-step semantics for call-by-need
• The call-by-need lambda calculus
• The Call-by-Need Lambda Calculus, Revisited

Cites work

• A semantics for lambda calculi with resources
• An Unsolvable Problem of Elementary Number Theory
• Call-by-name, call-by-value and the \(\lambda\)-calculus
• Call-by-need, neededness and all that
• Codifying guarded definitions with recursive schemes
• Coinductive big-step operational semantics
• Combinatory logic. With two sections by William Craig.
• Deriving a lazy abstract machine
• Formal verification of the correspondence between call-by-need and call-by-name
• scientific article; zbMATH DE number 1088036 (Why is no real title available?)
• scientific article; zbMATH DE number 3400430 (Why is no real title available?)
• Implementing lazy functional languages on stock hardware: the Spineless Tagless G-machine
• Infinite objects in type theory
• Needed reduction and spine strategies for the lambda calculus
• Small-step and big-step semantics for call-by-need
• The adequacy of Launchbury's natural semantics for lazy evaluation
• The call-by-need lambda calculus
• The call-by-need lambda calculus
• The locally nameless representation
• The Mechanical Evaluation of Expressions
• Types and programing languages

This page was built for publication: Formal verifications of call-by-need and call-by-name evaluations with mutual recursion

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