Strong normalization property for second order linear logic

DOI10.1016/J.TCS.2009.07.053MaRDI QIDQ1044837zbMATH OpenOpenAlexFDO

Authors Michele Pagani, Lorenzo Tortora de Falco

Publication date 15 December 2009

Published in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/j.tcs.2009.07.053

zbMATH Keywords

additive connectivesconfluencelinear logicproof-netssliced pure structuresstandardizationweak normalization

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42)

Recommendations

• Linear Logic and Strong Normalization
• A direct proof of strong normalization for full constructive second-order logic
• A semantic account of strong normalization in linear logic
• Strong normalization of a symmetric lambda calculus for second-order classical logic
• A strong normalization result for classical logic
• Proofs of strong normalisation for second order classical natural deduction
• scientific article; zbMATH DE number 2242601
• On proof normalization in linear logic
• Strong logics of first and second order
• scientific article; zbMATH DE number 2080223

Cites work

• A new deconstructive logic: linear logic
• Additives of linear logic and normalization. I: A (restricted) Church-Rosser property.
• Confluence of Pure Differential Nets with Promotion
• scientific article; zbMATH DE number 4033738 (Why is no real title available?)
• scientific article; zbMATH DE number 3735770 (Why is no real title available?)
• scientific article; zbMATH DE number 46869 (Why is no real title available?)
• scientific article; zbMATH DE number 108365 (Why is no real title available?)
• scientific article; zbMATH DE number 2134916 (Why is no real title available?)
• scientific article; zbMATH DE number 1889386 (Why is no real title available?)
• scientific article; zbMATH DE number 937366 (Why is no real title available?)
• scientific article; zbMATH DE number 3275554 (Why is no real title available?)
• Intuitionistic differential nets and lambda-calculus
• Linear logic
• Phase semantic cut-elimination and normalization proofs of first- and higher-order linear logic
• Polarized and focalized linear and classical proofs
• Proof nets and explicit substitutions
• Strong normalization from weak normalization in typed \(\lambda\)-calculi
• The lambda calculus. Its syntax and semantics. Rev. ed.

Cited in

(21)

• A direct proof of strong normalization for full constructive second-order logic
• Cut elimination for a logic with induction and co-induction
• Proof nets for classical logic
• Quantitative classical realizability
• A semantic account of strong normalization in linear logic
• Linear Logic and Strong Normalization
• Realizability Proof for Normalization of Full Differential Linear Logic
• Confluence of Pure Differential Nets with Promotion
• Visible acyclic differential nets. I: Semantics
• Jump from parallel to sequential proofs: exponentials
• Preface to the special volume
• A semantic measure of the execution time in linear logic
• Intuitionistic differential nets and lambda-calculus
• The conservation theorem for differential nets
• Exponentials as Substitutions and the Cost of Cut Elimination in Linear Logic
• Exponentials as substitutions and the cost of cut elimination in linear logic
• Super exponentials in linear logic
• Infinitary cut-elimination via finite approximations
• Type isomorphisms for multiplicative-additive linear logic
• On the cut-elimination of the modal -calculus: linear logic to the rescue
• Confluence for proof-nets via parallel cut elimination

This page was built for publication: Strong normalization property for second order linear logic

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