# Normalisation of the theory $\mathbf{T}$ of Cartesian closed categories and conservativity of extensions $mathbfT\left[x\right]$ of $mathbfT$

RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications (1999)

- Volume: 33, Issue: 3, page 227-257
- ISSN: 0988-3754

## Access Full Article

top## How to cite

topPreller, Anne, and Duroux, P.. "Normalisation of the theory $\mathbf {T}$ of Cartesian closed categories and conservativity of extensions $mathbf{T}[x]$ of $mathbf{T}$." RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications 33.3 (1999): 227-257. <http://eudml.org/doc/92601>.

@article{Preller1999,

author = {Preller, Anne, Duroux, P.},

journal = {RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications},

keywords = {Cartesian closed categories; simply typed lambda calculus; rewrite system; graph of generators; inductive definition of normal terms; decidability; functional completeness},

language = {eng},

number = {3},

pages = {227-257},

publisher = {EDP-Sciences},

title = {Normalisation of the theory $\mathbf \{T\}$ of Cartesian closed categories and conservativity of extensions $mathbf\{T\}[x]$ of $mathbf\{T\}$},

url = {http://eudml.org/doc/92601},

volume = {33},

year = {1999},

}

TY - JOUR

AU - Preller, Anne

AU - Duroux, P.

TI - Normalisation of the theory $\mathbf {T}$ of Cartesian closed categories and conservativity of extensions $mathbf{T}[x]$ of $mathbf{T}$

JO - RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications

PY - 1999

PB - EDP-Sciences

VL - 33

IS - 3

SP - 227

EP - 257

LA - eng

KW - Cartesian closed categories; simply typed lambda calculus; rewrite system; graph of generators; inductive definition of normal terms; decidability; functional completeness

UR - http://eudml.org/doc/92601

ER -

## References

top- [1] T. Altenkirch, M. Hofmann and T. Streicher, Categorical reconstruction of a reduction free normalisation proof, preliminary version, P. Dybjer and R. Pollacks, Eds., Proceedings CTCS '95, Springer, Lecture Notes in Computer Science 953 (1995) 182-199. MR1463721
- [2] U. Berger and H. Schwichtenberg, An inverse to the evaluation functional for typed λ-calculus, in Proc. of the 6th Annual IEEE Symposium of Logic in Computer Science (1991) 203-211.
- [3] D. Cubric', Embedding of a free Cartesian Closed Category in the Category of Sets. J. Pure and Applied Algebra (to appear). Zbl0898.18004MR1600522
- [4] D. Cubric', P. Dybjer and P. Scott, Normalization and the Yoneda Embedding, MSCS 8 (1998) 153-192. Zbl0918.03012MR1618366
- [5] R. Di Cosmo, Isomorphisms of Types, Birkhaeuser (1995). Zbl0819.03006
- [6] K. Došen and Z. Petric', The maximality of Cartesian Categories, Rapport Institut de Recherche de Toulouse, CNRS, 97-42-R (1997). Zbl0978.18001
- [7] J. Lambek and P. J. Scott, Introduction to Higher Order Categorical Logic, Cambridge University Press (1989). Zbl0596.03002MR856915
- [8] A. Obtulowicz, Algebra of constructions I. The word problem for partial algebras. Inform. and Comput. 73 (1987) 29-173. Zbl0653.03010MR883492

## NotesEmbed ?

topTo embed these notes on your page include the following JavaScript code on your page where you want the notes to appear.