Strong normalization property for second order linear logic
From MaRDI portal
Publication:1044837
DOI10.1016/j.tcs.2009.07.053zbMath1186.68240OpenAlexW2113402167MaRDI QIDQ1044837
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
weak normalizationlinear logicconfluencestandardizationproof-netsadditive connectivessliced pure structures
Related Items (13)
A semantic account of strong normalization in linear logic ⋮ Jump from parallel to sequential proofs: exponentials ⋮ Visible acyclic differential nets. I: Semantics ⋮ Exponentials as Substitutions and the Cost of Cut Elimination in Linear Logic ⋮ The conservation theorem for differential nets ⋮ Cut elimination for a logic with induction and co-induction ⋮ Proof nets for classical logic ⋮ Realizability Proof for Normalization of Full Differential Linear Logic ⋮ Preface to the special volume ⋮ A semantic measure of the execution time in linear logic ⋮ Intuitionistic differential nets and lambda-calculus ⋮ Confluence of Pure Differential Nets with Promotion ⋮ Quantitative classical realizability
Cites Work
- Intuitionistic differential nets and lambda-calculus
- Polarized and focalized linear and classical proofs
- Linear logic
- The lambda calculus. Its syntax and semantics. Rev. ed.
- Strong normalization from weak normalization in typed \(\lambda\)-calculi
- Additives of linear logic and normalization. I: A (restricted) Church-Rosser property.
- Phase semantic cut-elimination and normalization proofs of first- and higher-order linear logic
- Confluence of Pure Differential Nets with Promotion
- A new deconstructive logic: linear logic
- Proof nets and explicit substitutions
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
This page was built for publication: Strong normalization property for second order linear logic
