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

• Type: Journal
• Year: 2010
• Where: TCS
• Authors: Michele Pagani, Lorenzo Tortora de Falco
• Keywords: Pure Structures, Standardization, TCS 2010, Theoretical Computer Science, first Complete Proof