Open call-by-value

DOI10.1007/978-3-319-47958-3_12zbMATH Open1483.68063arXiv1609.00322OpenAlexW2513611569MaRDI QIDQ3179293FDOQ3179293

Authors: Beniamino Accattoli, Giulio Guerrieri 

Publication date: 21 December 2016

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

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.

Full work available at URL: https://arxiv.org/abs/1609.00322

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

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)

Cites Work

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

Cited In (18)

• Call-by-value lambda calculus as a model of computation in Coq
• Title not available (Why is that?)
• (In)efficiency and reasonable cost models
• 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
• Title not available (Why is that?)
• 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

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)