scientific article; zbMATH DE number 786499

zbMATH Open0854.03011MaRDI QIDQ4842980FDOQ4842980

Authors: Vincent Danos, Laurent Regnier 

Publication date: 16 August 1995

Title of this publication is not available (Why is that?)

Recommendations

• Coherent models of proof nets
• Publication:4896506
• Sequent reconstruction in LLM -- A sweepline proof
• Homology of proof-nets
• Minimality of the correctness criterion for multiplicative proof nets

zbMATH Keywords

linear logicgeometry of interactionlambda-calculusproof netspersistent pathsregular paths

Mathematics Subject Classification ID

Cut-elimination and normal-form theorems (03F05) Combinatory logic and lambda calculus (03B40) Structure of proofs (03F07)

Cited In (37)

• On intuitionistic proof nets with additional rewrite rules and their approximations
• Title not available (Why is that?)
• Proof spaces for unbounded parallelism
• An abstract approach to stratification in linear logic
• Interactive observability in Ludics: the geometry of tests
• Title not available (Why is that?)
• A semantic account of strong normalization in linear logic
• The relational model is injective for multiplicative exponential linear logic (without weakenings)
• A semantic measure of the execution time in linear logic
• Interaction graphs: multiplicatives
• An Explicit Framework for Interaction Nets
• Interaction graphs: additives
• Polarized proof-nets and \(\lambda \mu\)-calculus
• The additive multiboxes
• Interaction combinators
• Additives of linear logic and normalization. I: A (restricted) Church-Rosser property.
• Paths-based criteria and application to linear logic subsystems characterizing polynomial time
• On paths-based criteria for polynomial time complexity in proof-nets
• Weak typed Böhm theorem on IMLL
• Proof nets and the call-by-value \(\lambda\)-calculus
• A \(\mathsf{MALL}\) geometry of interaction based on indexed linear logic
• Light logics and optimal reduction: completeness and complexity
• On the Functor ℓ2
• Reasonable space for the \(\lambda \)-calculus, logarithmically
• Geometry of resource interaction and Taylor-Ehrhard-Regnier expansion: \textit{a minimalist approach}
• Linear logic by levels and bounded time complexity
• Geometry of resource interaction -- \textit{a minimalist approach}
• Abstract machines, optimal reduction, and streams
• Exponentially handsome proof nets and their normalization
• Proofs as Polynomials
• A proof of the focusing theorem via MALL proof nets
• Title not available (Why is that?)
• Title not available (Why is that?)
• Conformal field theory as a nuclear functor
• Handshake games
• Observational equivalence for the interaction combinators and internal separation
• A categorical model for the geometry of interaction

This page was built for publication:

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