Open call-by-value

DOI10.1007/978-3-319-47958-3_12MaRDI QIDQ3179293zbMATH OpenOpenAlexFDO

Authors Beniamino Accattoli, Giulio Guerrieri

Publication date 21 December 2016

Published in Programming Languages and Systems (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1609.00322, https://hal.inria.fr/hal-01425465/file/Accattoli%2CGuerrieri-OpenCBV.pdf

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40) Proof-theoretic aspects of linear logic and other substructural logics (03F52) Functional programming and lambda calculus (68N18)

Abstract: The elegant theory of the call-by-value lambda-calculus relies on weak evaluation and closed terms, that are natural hypotheses in the study of programming languages. To model proof assistants, however, strong evaluation and open terms are required, and it is well known that the operational semantics of call-by-value becomes problematic in this case. Here we study the intermediate setting -- that we call Open Call-by-Value -- of weak evaluation with open terms, on top of which Gr'egoire and Leroy designed the abstract machine of Coq. Various calculi for Open Call-by-Value already exist, each one with its pros and cons. This paper presents a detailed comparative study of the operational semantics of four of them, coming from different areas such as the study of abstract machines, denotational semantics, linear logic proof nets, and sequent calculus. We show that these calculi are all equivalent from a termination point of view, justifying the slogan Open Call-by-Value.

Recommendations

• Implementing open call-by-value
• An Operational Account of Call-by-Value Minimal and Classical λ-Calculus in “Natural Deduction” Form
• Types of fireballs
• Call-by-value lambda calculus as a model of computation in Coq
• Weak call-by-value lambda calculus as a model of computation in Coq

Cites work

• scientific article; zbMATH DE number 4179333 (Why is no real title available?)
• scientific article; zbMATH DE number 1953273 (Why is no real title available?)
• scientific article; zbMATH DE number 2044494 (Why is no real title available?)
• scientific article; zbMATH DE number 236855 (Why is no real title available?)
• A Semantical and Operational Account of Call-by-Value Solvability
• A compiled implementation of strong reduction
• A reflection on call-by-value
• An Operational Account of Call-by-Value Minimal and Classical λ-Calculus in “Natural Deduction” Form
• An equivalence between lambda- terms
• Call-by-Value  -calculus and LJQ
• Call-by-name, call-by-value and the \(\lambda\)-calculus
• Call-by-name, call-by-value, call-by-need and the linear lambda calculus
• Call-by-value Solvability
• Call-by-value solvability, revisited
• Lazy strong normalization
• On the Relative Usefulness of Fireballs
• On the value of variables
• Proof nets and the call-by-value \(\lambda\)-calculus
• Standardization of a Call-By-Value Lambda-Calculus
• Strong normalization from an unusual point of view
• The duality of computation
• The duality of computation under focus
• The parametric lambda calculus. A metamodel for computation.
• The weak lambda calculus as a reasonable machine

Cited in

(18)

• Call-by-value lambda calculus as a model of computation in Coq
• (In)efficiency and reasonable cost models
• scientific article; zbMATH DE number 7526055 (Why is no real title available?)
• On reduction and normalization in the computational core
• The Negligible and Yet Subtle Cost of Pattern Matching
• Eager functions as processes
• Types of fireballs
• Z property for the shuffling calculus
• Strong call-by-value and multi types
• A Fresh Look at the λ-Calculus
• The bang calculus and the two Girard's translations
• The bang calculus revisited
• scientific article; zbMATH DE number 7226008 (Why is no real title available?)
• Light genericity
• The bang calculus revisited
• On the value of variables
• Weak call-by-value lambda calculus as a model of computation in Coq
• Implementing open call-by-value

Describes a project that uses

Uses Software

• Coq

This page was built for publication: Open call-by-value

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