The bang calculus revisited

DOI10.1007/978-3-030-59025-3_2OpenAlexW3090972609MaRDI QIDQ2039931

Antonio Bucciarelli, Alejandro Ríos, Delia Kesner, Andrés Viso

Publication date: 6 July 2021

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

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18) Logic programming (68N17)

Related Items

Plotkin's call-by-value \(\lambda\)-calculus as a modal calculus, Node Replication: Theory And Practice, Quantitative global memory, Factorization in call-by-name and call-by-value calculi via linear logic, The spirit of node replication, The bang calculus revisited, The bang calculus revisited, On reduction and normalization in the computational core

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• A semantic account of strong normalization in linear logic
• A type assignment for \(\lambda\)-calculus complete both for FPTIME and strong normalization
• A semantic measure of the execution time in linear logic
• Linear logic
• The lambda calculus. Its syntax and semantics. Rev. ed.
• Call-by-push-value: Decomposing call-by-value and call-by-name
• Uniformity and the Taylor expansion of ordinary lambda-terms
• Normal functors, power series and \(\lambda\)-calculus
• An extension of basic functionality theory for \(\lambda\)-calculus
• An equivalence between lambda- terms
• Call-by-name, call-by-value, call-by-need and the linear lambda calculus
• The bang calculus revisited
• Call-By-Push-Value from a Linear Logic Point of View
• Reasoning About Call-by-need by Means of Types
• Non-idempotent intersection types and strong normalisation
• Call-by-Value Solvability, Revisited
• Open Call-by-Value
• Quantitative Types for the Linear Substitution Calculus
• A new type assignment for λ-terms
• Solvability in Resource Lambda-Calculus
• The Structural λ-Calculus
• Execution time of λ-terms via denotational semantics and intersection types
• Non-idempotent intersection types for the Lambda-Calculus
• Tight typings and split bounds, fully developed
• The Relational Model Is Injective for Multiplicative Exponential Linear Logic
• A Semantical and Operational Account of Call-by-Value Solvability
• Taylor expansion for Call-By-Push-Value
• On phase semantics and denotational semantics: The exponentials
• Types by need
• Types of fireballs