Normalisation of the theory 𝐓 of Cartesian closed categories and conservativity of extensions m a t h b f T [ x ] of m a t h b f T

Anne Preller; P. Duroux

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

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

How to cite

top

Preller, 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. [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. [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. [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. [4] D. Cubric', P. Dybjer and P. Scott, Normalization and the Yoneda Embedding, MSCS 8 (1998) 153-192. Zbl0918.03012MR1618366
  5. [5] R. Di Cosmo, Isomorphisms of Types, Birkhaeuser (1995). Zbl0819.03006
  6. [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. [7] J. Lambek and P. J. Scott, Introduction to Higher Order Categorical Logic, Cambridge University Press (1989). Zbl0596.03002MR856915
  8. [8] A. Obtulowicz, Algebra of constructions I. The word problem for partial algebras. Inform. and Comput. 73 (1987) 29-173. Zbl0653.03010MR883492

NotesEmbed ?

top

You must be logged in to post comments.

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

Only the controls for the widget will be shown in your chosen language. Notes will be shown in their authored language.

Tells the widget how many notes to show per page. You can cycle through additional notes using the next and previous controls.

    
                

                
Note: Best practice suggests putting the JavaScript code just before the closing </body> tag.