Sign in
Author

Conference

Journal

Organization

Year

DOI
Look for results that meet for the following criteria:
since
equal to
before
between
and
Search in all fields of study
Limit my searches in the following fields of study
Agriculture Science
Arts & Humanities
Biology
Chemistry
Computer Science
Economics & Business
Engineering
Environmental Sciences
Geosciences
Material Science
Mathematics
Medicine
Physics
Social Science
Multidisciplinary
Keywords
(4)
Proof Net
Strong Normalization
Linear Logic
Second Order
Subscribe
Academic
Publications
Strong normalization property for second order linear logic
Strong normalization property for second order linear logic,10.1016/j.tcs.2009.07.053,Theoretical Computer Science,Michele Pagani,Lorenzo Tortora De F
Edit
Strong normalization property for second order linear logic
(
Citations: 5
)
BibTex

RIS

RefWorks
Download
Michele Pagani
,
Lorenzo Tortora De Falco
Abstract The paper contains the first complete proof of strong normali zation (SN) for full
second order
linear logic
(LL): Girard’s original proof uses a stan dardization theorem which is not proven. We introduce sliced pure structures (sps), a very general version of Girard’s proofnets, and we apply to sps Gandy’s method to infer SN from weak normalization (WN). We prove a standardization theorem for sps: if WN without erasing steps holds for an sps, then it enjoys SN. A key step in the proof of standardization is a confluence theorem for sps obtained by using only a very weak f orm of correctness, namely acyclicity slice by slice. We conclude by showing,how standardization for sps allows to prove SN of LL, using as usual Girard’s reducibility candidates. Key words: (weak strong) normalization, confluence, standardization , linear logic,
Journal:
Theoretical Computer Science  TCS
, vol. 411, no. 2, pp. 410444, 2010
DOI:
10.1016/j.tcs.2009.07.053
Cumulative
Annual
View Publication
The following links allow you to view full publications. These links are maintained by other sources not affiliated with Microsoft Academic Search.
(
www.sciencedirect.com
)
(
www.informatik.unitrier.de
)
(
dx.doi.org
)
Citation Context
(3)
...As is evident in [
10
], this is the first step in proving strong normalization in the typed case 2 . Furtherly, as can be deducted from [9],...
...Our technique, reminiscent of the work done on LL in [
10
], uses a finite development theorem used to prove a strong confluence property of a suitable notion of parallel reduction...
...One can already see two big differences with respect to LL and the work done with it in [
10
]: firstly, sums may arise even without the “logical” step of dereliction on box; moreover, the codereliction on box rule, which reduces a commutative cut, changes the possible cuts on all other cuts of the box...
...These problems prevent an immediate adaptation of the measures used in [
10
]...
...In [15], Danos proved the counterpart of the finite development theorem for MELL ,a nd Pagani and Tortora de Falco did the same for the whole of second order LL in [
10
]...
...It turns out that � λ� = 5184(12[3]+[8, 13, 13]), while � μ� = 900(9[3]+[7,
10
]), which is indeed lower (though in a quite coarse way)...
Paolo Tranquilli
.
Confluence of Pure Differential Nets with Promotion
...The fact that we used a specific reduction strategy in the proof of this lemma means that some more work would be needed if we were to prove strong normalisation of the system, as it was done by Pagani and Tortora de Falco for LL in [
8
]...
Stéphane Gimenez
.
Realizability Proof for Normalization of Full Differential Linear Logi...
...The way we manage these sums is very similar to the handling of linear logic additives in sliced proofnets (see [
PTdF07
])...
Michele Pagani
.
Visible acyclic differential nets, Part I: Semantics
References
(23)
A New Deconstructive Logic: Linear Logic
(
Citations: 103
)
Vincent Danos
,
Jeanbaptiste Joinet
,
Harold Schellinx
Journal:
Journal of Symbolic Logic  JSYML
, vol. 62, no. 3, pp. 755807, 1997
Proof Nets And Explicit Substitutions
(
Citations: 16
)
Roberto Di Cosmo
,
Delia Kesner
,
Emmanuel Polonovski
Journal:
Mathematical Structures in Computer Science  MSCS
, vol. 13, no. 3, pp. 409450, 2003
Proofs of strong normalization
(
Citations: 37
)
R. O. Gandy
Published in 1980.
Interpretation fonctionelle et #limination des coupures de l'arithm&ique d'ordre sup#rieur
(
Citations: 54
)
J. Y Girard
Published in 1972.
Proof Theory and Logical Complexity
(
Citations: 163
)
J. Y Girard
Published in 1987.
Sort by:
Citations
(5)
A semantic measure of the execution time in linear logic
(
Citations: 4
)
Daniel de Carvalho
,
Michele Pagani
,
Lorenzo Tortora de Falco
Journal:
Theoretical Computer Science  TCS
, vol. 412, no. 20, pp. 18841902, 2011
Intuitionistic differential nets and lambdacalculus
(
Citations: 2
)
Paolo Tranquilli
Journal:
Theoretical Computer Science  TCS
, vol. 412, no. 20, pp. 19791997, 2011
Confluence of Pure Differential Nets with Promotion
Paolo Tranquilli
Conference:
Computer Science Logic  CSL
, pp. 500514, 2009
Realizability Proof for Normalization of Full Differential Linear Logic
Stéphane Gimenez
Visible acyclic differential nets, Part I: Semantics
Michele Pagani
Journal:
Annals of Pure and Applied Logic  APAL