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

DOI10.1007/978-3-030-34175-6_10zbMATH Open1542.68028MaRDI QIDQ6536314

Eijiro Sumii, Masayuki Mizuno

Publication date: 19 April 2024

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)

Cites Work

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

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)