scientific article; zbMATH DE number 786495
From MaRDI portal
Publication:4842976
zbMath0830.03028MaRDI QIDQ4842976
Publication date: 30 January 1996
Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.
sequentproof-netsinteraction netsDanos-Regnier correctness criterionmultiplicative-exponential fragment of linear logic
Grammars and rewriting systems (68Q42) Proof theory in general (including proof-theoretic semantics) (03F03) Subsystems of classical logic (including intuitionistic logic) (03B20)
Related Items
An Analytic Propositional Proof System on Graphs, Variable Binding, Symmetric Monoidal Closed Theories, and Bigraphs, Differential interaction nets, Interaction combinators, The geometry of Bayesian programming, Resource operators for \(\lambda\)-calculus, Natural deduction and coherence for weakly distributive categories, Interaction nets and term-rewriting systems, Unnamed Item, Visible acyclic differential nets. I: Semantics, The conservation theorem for differential nets, The relational model is injective for multiplicative exponential linear logic (without weakenings), Unnamed Item, Unnamed Item, Unnamed Item, Proof nets for classical logic, The graphical Krivine machine, Realizability Proof for Normalization of Full Differential Linear Logic, Light linear logic, Common Knowledge Logic in a Higher Order Proof Assistant, On intuitionistic proof nets with additional rewrite rules and their approximations, 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, Parsing MELL proof nets, Interpreting a finitary pi-calculus in differential interaction nets, Unnamed Item, Differential Linear Logic and Polarization, Light linear logic, Soft linear logic and polynomial time, Deep inference and expansion trees for second-order multiplicative linear logic, Unnamed Item, Proof diagrams for multiplicative linear logic: syntax and semantics, Interaction nets for linear logic, Skew confluence and the lambda calculus with letrec, Parallel beta reduction is not elementary recursive, Encoding linear logic with interaction combinators, Universal Boolean Systems, Intensional Properties of Polygraphs, Rewritings for Polarized Multiplicative and Exponential Proof Structures, A uniform semantic proof for cut-elimination and completeness of various first and higher order logics., Token-passing Nets for Functional Languages
