Intuitionistic differential nets and lambda-calculus

DOI10.1016/J.TCS.2010.12.022MaRDI QIDQ534707zbMATH OpenOpenAlexFDO

Authors Paolo Tranquilli

Publication date 10 May 2011

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

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

zbMATH Keywords

linear logicconfluencelambda-calculusnormalizationproof netsdifferential interaction netsexponential reduction

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40) Structure of proofs (03F07) Proof-theoretic aspects of linear logic and other substructural logics (03F52)

Recommendations

• Differential interaction nets
• The conservation theorem for differential nets
• The differential lambda-calculus
• The differential \(\lambda \mu\)-calculus
• Resource operators for \(\lambda\)-calculus

Cites work

• scientific article; zbMATH DE number 786495 (Why is no real title available?)
• scientific article; zbMATH DE number 1405619 (Why is no real title available?)
• A linearization of the Lambda-calculus and consequences
• A semantics for lambda calculi with resources
• An equivalence between lambda- terms
• Differential interaction nets
• Finiteness spaces
• Linear logic
• On Köthe sequence spaces and linear logic
• On Linear Combinations of λ-Terms
• Polarized proof-nets and \(\lambda \mu\)-calculus
• Strong normalization property for second order linear logic
• The differential \(\lambda \mu\)-calculus
• The differential lambda-calculus
• The structure of multiplicatives
• Uniformity and the Taylor expansion of ordinary lambda-terms

Cited in

(18)

• Behavioural differential equations: a coinductive calculus of streams, automata, and power series
• A deep inference system for differential linear logic
• The conservation theorem for differential nets
• Böhm's theorem for resource lambda calculus through Taylor expansion
• Relational graph models, Taylor expansion and extensionality
• scientific article; zbMATH DE number 7566060 (Why is no real title available?)
• Strong normalization property for second order linear logic
• Visible acyclic differential nets. I: Semantics
• Differential interaction nets
• Interpreting a finitary pi-calculus in differential interaction nets
• Resource operators for \(\lambda\)-calculus
• Confluence of Pure Differential Nets with Promotion
• Transport of finiteness structures and applications
• Proof nets and the call-by-value \(\lambda\)-calculus
• Realizability Proof for Normalization of Full Differential Linear Logic
• Geometry of resource interaction and Taylor-Ehrhard-Regnier expansion: \textit{a minimalist approach}
• The differential lambda-calculus
• The Separation Theorem for Differential Interaction Nets

This page was built for publication: Intuitionistic differential nets and lambda-calculus

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q534707)