Sciweavers

Share
TCS
2010

Strong normalization property for second order linear logic

11 years 3 months ago
Strong normalization property for second order linear logic
The paper contains the first complete proof of strong normalization (SN) for full second order linear logic (LL): Girard’s original proof uses a standardization 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 our proof of standardization is a confluence theorem for sps obtained by using only a very weak form 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, proof-nets, additive connectives, sliced pure structures
Michele Pagani, Lorenzo Tortora de Falco
Added 30 Jan 2011
Updated 30 Jan 2011
Type Journal
Year 2010
Where TCS
Authors Michele Pagani, Lorenzo Tortora de Falco
Comments (0)
books