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

https://hal.inria.fr/inria-00211877
Contributor : Brauner Paul <>
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

paper.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : inria-00211877, version 1

Collections

Citation

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

Share

Metrics

Record views

329

Files downloads

193