HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information
Skip to Main content Skip to Navigation
Preprints, Working Papers, ...

A semantic normalization proof for a system with recursors

Lisa Allali 1 Paul Brauner 2
2 PAREO - Formal islands: foundations and applications
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : Semantics methods have been used to prove cut elimination theorems for a long time. It is only recently that they have been extend to prove strong normalization results, in particular for theories in deduction modulo. However such semantic methods did not apply for systems with recursors like Godel system T. We show in this paper how super natural deduction provides a bridge between superconsistency of arithmetic and strong normalization of system T. We then generalize this result to a family of inductive types before discussing the dependant case.
Document type :
Preprints, Working Papers, ...
Complete list of metadata

Cited literature [28 references]  Display  Hide  Download

Contributor : Brauner Paul Connect in order to contact the contributor
Submitted on : Tuesday, January 22, 2008 - 10:29:31 AM
Last modification on : Friday, February 26, 2021 - 3:28:08 PM
Long-term archiving on: : Thursday, April 15, 2010 - 1:56:27 AM


Files produced by the author(s)


  • HAL Id : inria-00211877, version 1



Lisa Allali, Paul Brauner. A semantic normalization proof for a system with recursors. 2008. ⟨inria-00211877⟩



Record views


Files downloads