Strong normalization of proof nets modulo structural congruences

DOI10.1007/3-540-48685-2_6MaRDI QIDQ4938598zbMATH OpenFDO

Authors Roberto Di Cosmo, Stefano Guerrini

Publication date 23 February 2000

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/3-540-48685-2_6

zbMATH Keywords

\(\lambda\)-calculuslinear logicparallel syntaxproof netsrewritingstrong normalization

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40) Structure of proofs (03F07) Proof-theoretic aspects of linear logic and other substructural logics (03F52)

Recommendations

• Linear Logic and Strong Normalization
• scientific article; zbMATH DE number 937366
• A semantic account of strong normalization in linear logic
• Coherence for sharing proof nets
• On intuitionistic proof nets with additional rewrite rules and their approximations

Cited in

(11)

• A direct proof of strong normalization for full constructive second-order logic
• A new machine-checked proof of strong normalisation for display logic
• Confluence of Pure Differential Nets with Promotion
• On intuitionistic proof nets with additional rewrite rules and their approximations
• scientific article; zbMATH DE number 7599997 (Why is no real title available?)
• Proof normalization for resolution and paramodulation
• Intuitionistic differential nets and lambda-calculus
• The conservation theorem for differential nets
• Type isomorphisms for multiplicative-additive linear logic
• Confluence for proof-nets via parallel cut elimination
• Resource operators for \(\lambda\)-calculus

This page was built for publication: Strong normalization of proof nets modulo structural congruences

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4938598)