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

Strong normalization property for second order linear logic   (Citations: 5)
BibTex | RIS | RefWorks Download
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 proof-nets, 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. 410-444, 2010
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.
    • ...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 proof-nets (see [PTdF07])...

    Michele Pagani. Visible acyclic differential nets, Part I: Semantics

Sort by: