scientific article; zbMATH DE number 786495

MaRDI QIDQ4842976zbMATH OpenFDO

Authors Yves Lafont

Publication date 30 January 1996

zbMATH Keywords

Danos-Regnier correctness criterioninteraction netsmultiplicative-exponential fragment of linear logicproof-netssequent

Mathematics Subject Classification ID

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

Recommendations

• scientific article; zbMATH DE number 937366
• Proof diagrams for multiplicative linear logic
• Coherent models of proof nets
• Computer Science Logic

Cited in

(50)

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

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)