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

• A compiled implementation of strong reduction
• A reflection on call-by-value
• A Semantical and Operational Account of Call-by-Value Solvability
• An equivalence between lambda- terms
• An Operational Account of Call-by-Value Minimal and Classical λ-Calculus in “Natural Deduction” Form
• 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
• Call-by-Value  -calculus and LJQ
• 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?)
• 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

(26)

• Weak call-by-value lambda calculus as a model of computation in Coq
• The bang calculus revisited
• Implementing open call-by-value
• Eager functions as processes
• Call-by-value lambda calculus as a model of computation in Coq
• (In)efficiency and reasonable cost models
• On the value of variables
• Revisiting call-by-value Böhm trees in light of their Taylor expansion
• The bang calculus and the two Girard's translations
• The Negligible and Yet Subtle Cost of Pattern Matching
• Towards a semantic measure of the execution time in call-by-value lambda-calculus
• A Fresh Look at the λ-Calculus
• On reduction and normalization in the computational core
• Z property for the shuffling calculus
• The bang calculus revisited
• Types of fireballs
• Strong call-by-value and multi types
• Light genericity
• Positive focusing is directly useful
• Factorize factorization
• A fresh inductive approach to useful call-by-value
• Mirroring call-by-need, or values acting silly
• A quantitative approach to global state composition
• Genericity through stratification
• The benefits of diligence
• Mirroring call-by-need, or values acting silly

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)