Polarized and focalized linear and classical proofs

DOI10.1016/j.apal.2004.11.002zbMath1064.03035OpenAlexW2092580587MaRDI QIDQ556824

Lorenzo Tortora de Falco, Olivier Laurent, Myriam Quatrini

Publication date: 23 June 2005

Published in: Annals of Pure and Applied Logic (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.apal.2004.11.002

zbMATH Keywords

Classical logicCut-eliminationDenotational semanticsFocalizationLinear logicPolarizationProof-netsReversion

Mathematics Subject Classification ID

Cut-elimination and normal-form theorems (03F05) Structure of proofs (03F07) Proof-theoretic aspects of linear logic and other substructural logics (03F52)

Related Items

A focused approach to combining logics, Proof nets for classical logic, Focusing and polarization in linear, intuitionistic, and classical logics, Strong normalization property for second order linear logic, Syntax vs. semantics: A polarized approach

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Linear logic
• Computational isomorphisms in classical logic
• Additives of linear logic and normalization. I: A (restricted) Church-Rosser property.
• Polarized proof-nets and \(\lambda \mu\)-calculus
• The additive multiboxes
• A denotational semantics of \(LC2\)
• Classical isomorphisms of types
• A new constructive logic: classic logic
• A new deconstructive logic: linear logic
• SN and CR for free-style LK^tq: linear decorations and simulation of normalization