The differential lambda-calculus
From MaRDI portal
Publication:1884894
DOI10.1016/S0304-3975(03)00392-XzbMath1070.68020OpenAlexW2088376608MaRDI QIDQ1884894
Thomas Ehrhard, Laurent Regnier
Publication date: 27 October 2004
Published in: Theoretical Computer Science (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1016/s0304-3975(03)00392-x
Related Items (89)
Models of Linear Logic based on the Schwartz $\varepsilon$-product ⋮ Cartesian differential categories as skew enriched categories ⋮ What is a categorical model of the differential and the resource λ-calculi? ⋮ Relational graph models, Taylor expansion and extensionality ⋮ Unnamed Item ⋮ Taylor expansion, finiteness and strategies ⋮ Finiteness spaces and generalized power series ⋮ The differential \(\lambda \mu\)-calculus ⋮ Unnamed Item ⋮ Categorical Models for Simply Typed Resource Calculi ⋮ A Simply Typed λ-Calculus of Forward Automatic Differentiation ⋮ Differential interaction nets ⋮ Linear logic in normed cones: probabilistic coherence spaces and beyond ⋮ Unnamed Item ⋮ Differential logical relations. II: Increments and derivatives ⋮ An introduction to differential linear logic: proof-nets, models and antiderivatives ⋮ Transport of finiteness structures and applications ⋮ Order algebras: a quantitative model of interaction ⋮ The categorified Heisenberg algebra. I: A combinatorial representation. ⋮ An embedding theorem for tangent categories ⋮ Modeling linear logic with implicit functions ⋮ The linear-non-linear substitution 2-monad ⋮ Non-Deterministic Functions as Non-Deterministic Processes (Extended Version) ⋮ Visible acyclic differential nets. I: Semantics ⋮ Categorical models of the differential λ-calculus ⋮ Coherent differentiation ⋮ The conservation theorem for differential nets ⋮ A coherent differential PCF ⋮ Finitary Simulation of Infinitary $\beta$-Reduction via Taylor Expansion, and Applications ⋮ Correctness of automatic differentiation via diffeologies and categorical gluing ⋮ Unnamed Item ⋮ On operads, bimodules and analytic functors ⋮ Mackey-complete spaces and power series – a topological model of differential linear logic ⋮ Linearizing Combinators ⋮ Linear-algebraic λ-calculus: higher-order, encodings, and confluence. ⋮ Cartesian differential categories revisited ⋮ Unnamed Item ⋮ On Banach spaces of sequences and free linear logic exponential modality ⋮ Integral categories and calculus categories ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Weighted models for higher-order computation ⋮ Unnamed Item ⋮ Quantum computation: from a programmer's perspective ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Encodings of Turing machines in linear logic ⋮ Cofree coalgebras and differential linear logic ⋮ Convenient antiderivatives for differential linear categories ⋮ Densities of almost surely terminating probabilistic programs are differentiable almost everywhere ⋮ Geometry of resource interaction and Taylor–Ehrhard–Regnier expansion: a minimalist approach ⋮ Uniformity and the Taylor expansion of ordinary lambda-terms ⋮ Realizability Proof for Normalization of Full Differential Linear Logic ⋮ Böhm’s Theorem for Resource Lambda Calculus through Taylor Expansion ⋮ The shuffle quasimonad and modules with differentiation and integration ⋮ Categorical models of the differential \(\lambda\)-calculus revisited ⋮ Constructing Differential Categories and Deconstructing Categories of Games ⋮ A Tangent Category Alternative to the Fa\`a di Bruno Construction ⋮ A typed, algebraic, computational lambda-calculus ⋮ The vectorial \(\lambda\)-calculus ⋮ Differential algebras in codifferential categories ⋮ Intuitionistic differential nets and lambda-calculus ⋮ A linear category of polynomial diagrams ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Differential structure, tangent structure, and SDG ⋮ Unnamed Item ⋮ A categorical construction for the computational definition of vector spaces ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Exponential functions in Cartesian differential categories ⋮ Polynomial time over the reals with parsimony ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Strong Normalizability as a Finiteness Structure via the Taylor Expansion of $$\lambda $$ λ -terms ⋮ Differential Linear Logic and Polarization ⋮ Differential categories revisited ⋮ On the Taylor expansion of probabilistic λ-terms ⋮ The algebraic lambda calculus ⋮ Affine geometric spaces in tangent categories ⋮ Jets and differential linear logic ⋮ Dynamic game semantics ⋮ From Kruskal’s theorem to Friedman’s gap condition ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Term Collections in λ and ρ-calculi ⋮ Classical lambda calculus in modern dress
Uses Software
Cites Work
This page was built for publication: The differential lambda-calculus