scientific article; zbMATH DE number 786495

MaRDI QIDQ4842976zbMATH OpenFDO

Authors Yves Lafont

Publication date 30 January 1996

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)

Recommendations

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

Cited in

(49)

• Encoding linear logic with interaction combinators
• Proof diagrams for multiplicative linear logic
• 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
• Visible acyclic differential nets. I: Semantics
• Deep inference and expansion trees for second-order multiplicative linear logic
• The conservation theorem for differential nets
• scientific article; zbMATH DE number 7559284 (Why is no real title available?)
• An Interaction Net Encoding of Gödel’s System  $$\mathcal {T}$$
• scientific article; zbMATH DE number 937366 (Why is no real title available?)
• Parsing MELL proof nets
• scientific article; zbMATH DE number 1231514 (Why is no real title available?)
• Differential Linear Logic and Polarization
• The relational model is injective for multiplicative exponential linear logic (without weakenings)
• scientific article; zbMATH DE number 7003195 (Why is no real title available?)
• Light linear logic
• Interpreting a finitary pi-calculus in differential interaction nets
• The structure of interaction
• 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
• scientific article; zbMATH DE number 2134911 (Why is no real title available?)
• Soft linear logic and polynomial time
• Skew confluence and the lambda calculus with letrec
• scientific article; zbMATH DE number 7359406 (Why is no real title available?)
• Interaction nets and term-rewriting systems
• Exponentially handsome proof nets and their normalization
• 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
• Rewritings for polarized multiplicative and exponential proof structures
• Universal Boolean systems
• scientific article; zbMATH DE number 7471682 (Why is no real title available?)
• 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)