Uniformity and the Taylor expansion of ordinary lambda-terms

DOI10.1016/j.tcs.2008.06.001zbMath1154.68354OpenAlexW2007411063MaRDI QIDQ944386

Laurent Regnier, Thomas Ehrhard

Publication date: 16 September 2008

Published in: Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.tcs.2008.06.001

zbMATH Keywords

linear logicdenotational semanticslambda-calculusdifferential lambda-calculuslambda-calculus with multiplicitieslambda-calculus with resources

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18)

Related Items (34)

A semantic account of strong normalization in linear logic ⋮ What is a categorical model of the differential and the resource λ-calculi? ⋮ Relational graph models, Taylor expansion and extensionality ⋮ Taylor expansion, finiteness and strategies ⋮ Parsimonious Types and Non-uniform Computation ⋮ The differential \(\lambda \mu\)-calculus ⋮ Unnamed Item ⋮ Categorical Models for Simply Typed Resource Calculi ⋮ Differential interaction nets ⋮ Unnamed Item ⋮ An introduction to differential linear logic: proof-nets, models and antiderivatives ⋮ The Scott model of linear logic is the extensional collapse of its relational model ⋮ Coherent differentiation ⋮ Structural rules and algebraic properties of intersection types ⋮ Finitary Simulation of Infinitary $\beta$-Reduction via Taylor Expansion, and Applications ⋮ Non-idempotent intersection types in logical form ⋮ Unnamed Item ⋮ A Truly Concurrent Game Model of the Asynchronous $$\pi $$-Calculus ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Geometry of resource interaction and Taylor–Ehrhard–Regnier expansion: a minimalist approach ⋮ Realizability Proof for Normalization of Full Differential Linear Logic ⋮ Böhm’s Theorem for Resource Lambda Calculus through Taylor Expansion ⋮ A semantic measure of the execution time in linear logic ⋮ Intuitionistic differential nets and lambda-calculus ⋮ Unnamed Item ⋮ The bang calculus revisited ⋮ Unnamed Item ⋮ The bang calculus revisited ⋮ Strong Normalizability as a Finiteness Structure via the Taylor Expansion of $$\lambda $$ λ -terms ⋮ Differential Linear Logic and Polarization ⋮ On the Taylor expansion of probabilistic λ-terms ⋮ Jets and differential linear logic ⋮ Infinitary affine proofs

Uses Software

• Automath

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Linear logic
• Differential interaction nets
• The system \({\mathcal F}\) of variable types, fifteen years later
• Reversible, irreversible and optimal \(\lambda\)-machines
• The differential lambda-calculus
• The differential \(\lambda \mu\)-calculus
• A call-by-name lambda-calculus machine
• Locus Solum: From the rules of logic to the logic of rules
• A linearization of the Lambda-calculus and consequences
• A semantics for lambda calculi with resources
• Finiteness spaces
• Logical Approaches to Computational Barriers
• On phase semantics and denotational semantics: The exponentials

This page was built for publication: Uniformity and the Taylor expansion of ordinary lambda-terms