An introduction to differential linear logic: proof-nets, models and antiderivatives

DOI10.1017/S0960129516000372zbMath1456.03097arXiv1606.01642OpenAlexW2409783831MaRDI QIDQ4577980

Thomas Ehrhard

Publication date: 7 August 2018

Published in: Mathematical Structures in Computer Science (Search for Journal in Brave)

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

Mathematics Subject Classification ID

Proof-theoretic aspects of linear logic and other substructural logics (03F52)

Related Items (19)

Cartesian differential categories as skew enriched categories ⋮ Unnamed Item ⋮ Coherent differentiation ⋮ Mackey-complete spaces and power series – a topological model of differential linear logic ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Encodings of Turing machines in linear logic ⋮ Cofree coalgebras and differential linear logic ⋮ Reverse AD at higher types: pure, principled and denotationally correct ⋮ Differential algebras in codifferential categories ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Exponential functions in Cartesian differential categories ⋮ Jets and differential linear logic ⋮ Unnamed Item ⋮ Unnamed Item

Uses Software

• Automath

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• The Scott model of linear logic is the extensional collapse of its relational model
• Linear logic
• Computational interpretations of linear logic
• Uniformity and the Taylor expansion of ordinary lambda-terms
• Typed lambda calculi and applications. 9th international conference, TLCA 2009, Brasilia, Brazil, July 1--3, 2009. Proceedings
• The system \({\mathcal F}\) of variable types, fifteen years later
• Normal functors, power series and \(\lambda\)-calculus
• Handsome proof-nets: Perfect matchings and cographs
• Reversible, irreversible and optimal \(\lambda\)-machines
• The differential lambda-calculus
• The differential \(\lambda \mu\)-calculus
• A call-by-name lambda-calculus machine
• A Calculus for Interaction Nets Based on the Linear Chemical Abstract Machine
• Full Abstraction for Resource Calculus with Tests
• Realizability Proof for Normalization of Full Differential Linear Logic
• Differential categories
• Differential Structure in Models of Multiplicative Biadditive Intuitionistic Linear Logic
• The Cut-Elimination Theorem for Differential Nets with Promotion
• The algebraic lambda calculus
• Confluence of Pure Differential Nets with Promotion
• Transport of finiteness structures and applications
• A new correctness criterion for MLL proof nets
• A semantics for lambda calculi with resources
• On Köthe sequence spaces and linear logic
• The conservation theorem for differential nets
• Finiteness spaces
• Linear domains and linear maps
• Logical Approaches to Computational Barriers

This page was built for publication: An introduction to differential linear logic: proof-nets, models and antiderivatives