1. Strong normalization property for second order linear logic
- Author
-
Lorenzo Tortora de Falco, Michele Pagani, Laboratoire d'Informatique de Paris-Nord (LIPN), Université Paris 13 (UP13)-Institut Galilée-Université Sorbonne Paris Cité (USPC)-Centre National de la Recherche Scientifique (CNRS), Preuves, Programmes et Systèmes (PPS), Université Paris Diderot - Paris 7 (UPD7)-Centre National de la Recherche Scientifique (CNRS), Pagani, M, and TORTORA DE FALCO, Lorenzo
- Subjects
Normalization (statistics) ,Normalization property ,Correctness ,General Computer Science ,Linear logic ,0102 computer and information sciences ,01 natural sciences ,Linear ordering ,Theoretical Computer Science ,Proof-nets ,(Weak, strong) normalization ,(weakstrong)normalization ,0101 mathematics ,Mathematics ,proof-nets ,Discrete mathematics ,010102 general mathematics ,[INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO] ,Sliced pure structures ,Confluence ,16. Peace & justice ,Standardization ,010201 computation theory & mathematics ,confluence ,Additive connectives ,Algorithm ,Computer Science(all) - Abstract
International audience; 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.
- Published
- 2010