The adequacy of Launchbury's natural semantics for lazy evaluation

DOI10.1017/S0956796817000144zbMath1478.68137OpenAlexW2782154544MaRDI QIDQ4577822

Joachim Breitner

Publication date: 3 August 2018

Published in: Journal of Functional Programming (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1017/s0956796817000144

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18) Semantics in the theory of computing (68Q55) Formalization of mathematics in connection with theorem provers (68V20)

Related Items (3)

The Role of Indirections in Lazy Natural Semantics ⋮ Parberry’s pairwise sorting network revealed ⋮ Generic Authenticated Data Structures, Formally.

Uses Software

• Isabelle
• Isabelle/HOL
• Nominal Isabelle
• Locales
• Archive Formal Proofs
• Launchbury
• Call_Arity

Cites Work

• Locales: a module system for mathematical theories
• An operational semantics for parallel lazy evaluation
• The Role of Indirections in Lazy Natural Semantics
• Small-step and big-step semantics for call-by-need
• Deriving a lazy abstract machine
• General Bindings and Alpha-Equivalence in Nominal Isabelle

This page was built for publication: The adequacy of Launchbury's natural semantics for lazy evaluation