scientific article; zbMATH DE number 786499

MaRDI QIDQ4842980zbMATH OpenFDO

Authors Vincent Danos, Laurent Regnier

Publication date 16 August 1995

zbMATH Keywords

geometry of interactionlambda-calculuslinear logicpersistent pathsproof netsregular paths

Mathematics Subject Classification ID

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

Recommendations

• Coherent models of proof nets
• scientific article; zbMATH DE number 937366
• Sequent reconstruction in LLM -- A sweepline proof
• Homology of proof-nets
• Minimality of the correctness criterion for multiplicative proof nets

Cited in

(39)

• Linear logic by levels and bounded time complexity
• 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
• Polarized proof-nets and \(\lambda \mu\)-calculus
• The additive multiboxes
• An abstract approach to stratification in linear logic
• A semantic account of strong normalization in linear logic
• Proof spaces for unbounded parallelism
• Conformal field theory as a nuclear functor
• Handshake games
• Observational equivalence for the interaction combinators and internal separation
• On paths-based criteria for polynomial time complexity in proof-nets
• scientific article; zbMATH DE number 1231532 (Why is no real title available?)
• The relational model is injective for multiplicative exponential linear logic (without weakenings)
• Geometry of resource interaction and Taylor-Ehrhard-Regnier expansion: \textit{a minimalist approach}
• scientific article; zbMATH DE number 786497 (Why is no real title available?)
• On intuitionistic proof nets with additional rewrite rules and their approximations
• On the Functor ℓ2
• A \(\mathsf{MALL}\) geometry of interaction based on indexed linear logic
• Geometry of resource interaction -- \textit{a minimalist approach}
• Gluing resource proof-structures: inhabitation and inverting the Taylor expansion
• Abstract machines, optimal reduction, and streams
• A semantic measure of the execution time in linear logic
• Proofs as Polynomials
• scientific article; zbMATH DE number 5214898 (Why is no real title available?)
• An Explicit Framework for Interaction Nets
• A proof of the focusing theorem via MALL proof nets
• Light logics and optimal reduction: completeness and complexity
• Reasonable space for the -calculus, logarithmically
• Exponentially handsome proof nets and their normalization
• Confluence for proof-nets via parallel cut elimination
• Reasonable space for the -calculus, logarithmically
• Interaction graphs: multiplicatives
• Interactive observability in Ludics: the geometry of tests
• A categorical model for the geometry of interaction
• Weak typed Böhm theorem on IMLL
• Interaction graphs: additives
• Proof nets and the call-by-value \(\lambda\)-calculus

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)