scientific article; zbMATH DE number 786495

zbMATH Open0830.03028MaRDI QIDQ4842976FDOQ4842976

Authors: Yves Lafont 

Publication date: 30 January 1996

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

Recommendations

• Publication:4896506
• Proof diagrams for multiplicative linear logic
• Coherent models of proof nets
• Computer Science Logic

zbMATH Keywords

sequentproof-netsinteraction netsDanos-Regnier correctness criterionmultiplicative-exponential fragment of linear logic

Mathematics Subject Classification ID

Proof theory in general (including proof-theoretic semantics) (03F03) Grammars and rewriting systems (68Q42) Subsystems of classical logic (including intuitionistic logic) (03B20)

Cited In (49)

• Proof diagrams for multiplicative linear logic
• Encoding linear logic with interaction combinators
• A linear algorithm for MLL proof net correctness and sequentialization
• Correctness of linear logic proof structures is NL-complete
• On intuitionistic proof nets with additional rewrite rules and their approximations
• Interaction nets for linear logic
• Deep inference and expansion trees for second-order multiplicative linear logic
• The conservation theorem for differential nets
• Visible acyclic differential nets. I: Semantics
• Title not available (Why is that?)
• Parsing MELL proof nets
• Title not available (Why is that?)
• An Interaction Net Encoding of Gödel’s System  $$\mathcal {T}$$
• Title not available (Why is that?)
• Differential Linear Logic and Polarization
• Light linear logic
• The relational model is injective for multiplicative exponential linear logic (without weakenings)
• Title not available (Why is that?)
• The structure of interaction
• Interpreting a finitary pi-calculus in differential interaction nets
• Intuitionistic differential nets and lambda-calculus
• Differential interaction nets
• The graphical Krivine machine
• Proof diagrams for multiplicative linear logic: syntax and semantics
• Light linear logic
• A uniform semantic proof for cut-elimination and completeness of various first and higher order logics.
• Interaction combinators
• Intuitionistic multiplicative proof nets as models of directed acyclic graph descriptions
• Title not available (Why is that?)
• Soft linear logic and polynomial time
• Skew confluence and the lambda calculus with letrec
• Title not available (Why is that?)
• Exponentially handsome proof nets and their normalization
• Interaction nets and term-rewriting systems
• Variable Binding, Symmetric Monoidal Closed Theories, and Bigraphs
• Intensional properties of polygraphs
• Realizability Proof for Normalization of Full Differential Linear Logic
• Token-passing nets for functional languages
• Natural deduction and coherence for weakly distributive categories
• Resource operators for \(\lambda\)-calculus
• Parallel beta reduction is not elementary recursive
• The geometry of Bayesian programming
• Common knowledge logic in a higher order proof assistant
• Title not available (Why is that?)
• Rewritings for polarized multiplicative and exponential proof structures
• Universal Boolean systems
• An Analytic Propositional Proof System on Graphs
• From propositional to linear logic: An introduction. Decoration, simulation, normalization
• Proof nets for classical logic

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 Q4842976)