Sémantique catégorique des types : comprendre le système F

Pierre Argeron

Diagrammes (1988)

  • Volume: 19, page PA1-PA40
  • ISSN: 0224-3911

How to cite

top

Argeron, Pierre. "Sémantique catégorique des types : comprendre le système F." Diagrammes 19 (1988): PA1-PA40. <http://eudml.org/doc/193018>.

@article{Argeron1988,
author = {Argeron, Pierre},
journal = {Diagrammes},
keywords = {type in a category; algebraic theory of types; logical theory of types; Girard's system F of second order lambda-calculus},
language = {fre},
pages = {PA1-PA40},
publisher = {Université Paris 7, Unité d'enseignement et de recherche de mathématiques},
title = {Sémantique catégorique des types : comprendre le système F},
url = {http://eudml.org/doc/193018},
volume = {19},
year = {1988},
}

TY - JOUR
AU - Argeron, Pierre
TI - Sémantique catégorique des types : comprendre le système F
JO - Diagrammes
PY - 1988
PB - Université Paris 7, Unité d'enseignement et de recherche de mathématiques
VL - 19
SP - PA1
EP - PA40
LA - fre
KW - type in a category; algebraic theory of types; logical theory of types; Girard's system F of second order lambda-calculus
UR - http://eudml.org/doc/193018
ER -

References

top
  1. [Ageron-Even] Pierre Ageron et Christian Even: Etude de la catégorie des catégories cartésiennes fermées, à paraître. 
  2. [Barendregt84] Hendrik Pieter Barendregt; The lambda calculus, deuxième édition, North-Holland, 1984. MR774952
  3. [Burroni 8I] Albert Burroni: Algèbres graphiques, Cahiers de Topologie et Géométrie Différentielle, vol. XXII-3, Amiens, 1981. Zbl0497.18004
  4. [Coppey84] Laurent Coppey: Catégories de Peano, catégories algorithmiques, récursivité, Diagrammes 12, Paris, 1984. Zbl0565.18004MR800498
  5. [Coppey-Lair85] Laurent Coppey et Christian Lair: Algébricité, monadicité, esquissabilité et non-algébricité, Diagrammes 13, Paris, 1985. Zbl0594.18006MR817075
  6. [Coquand-Huet87] Thierry Coquand et Gérard Huet: Concepts mathématiques et informatiques formalisés dans le calcul des constructions, in Logic Colloquium 85, edited by Paris Logic Group, North-Holland, 1987. Zbl0627.03045MR895642
  7. [Coquand-Ehrhard87] Thierry Coquand et Thomas Ehrhard: An equational presentation of higher order logic, in Proceedings of Category Theory and Computer Science, edited by D, H. Pitt, A. Poigné, D. E. Rydeheard, Lect. Notes in Comp. Sci. 283, Springer, 1987, Zbl0643.03050MR925223
  8. [Coquand] Thierry Coquand: Categories of embeddings, à paraître. Zbl0688.18004
  9. [Curien86] Pierre-Louis Curien: Categorical combinators, Sequential Algorithms and Functional Programming, Pitman, 1986. 
  10. [Dubuc-Kelly83] Eduardo Dubuc et Max G. Kelly: A presentation of topoï as algebraic relative to categories or graphs, Journal of Algebra, vol. 81-2, 1983. Zbl0516.18009MR700293
  11. [Ehresmann68] Charles Ehresmann: Esquisses et types des structures algébriques, Bul. Instit, Polit. Iasi, vol. XIV, 1968. Zbl0196.03102MR238918
  12. [Freyd-Girard-Scedrov-Scott] Peter J. Freyd, Jean-Yves Girard, Andre Scedov et Philip J. Scott: Semantic parametricity in polymorphic μ-calculus, à paraître. 
  13. [Girard7l] Jean-Yves Girard: Une extension de l'interprétation fonctionnelle de Gödel à l'analyse et son application à l'élimination des coupures dans l'analyse et la théorie des types, in Proceedings of the second Scandinavian Logic Symposium, Oslo, 1970, edited by J.E Fenstad, North-Holland, 1971, Zbl0221.02013MR409133
  14. [Girard86] Jean-Yves Girard: The system F of variable types, fifteen years later, Theoretical Computer Science, vol. 45, 1986. Zbl0623.03013MR867281
  15. [Girard] Jean-Yves Girard: Typed μ-calculus, Cambridge Tracts in Theoretical Computer science, à paraître, 
  16. [Guitart-Lair80] René Guitart et Christian Lair; Calcul syntaxique des modèles et calcul des formules internes, Diagrammes 4, Paris, 1980. Zbl0508.03030MR684746
  17. [Huet] Gérard Huet: A uniform approach to type theory, à paraître. 
  18. [Lair75] Christian Lair: Esquissabilité et triblabilité, 21ème colloque sur les catégories, Amiens 75, Cahiers de Topologie et Géométrie Différentielle, vol. XVI-3, Amiens, 1975. Zbl0397.18006
  19. [Lair87] Christian Lair: Trames et sémantiques catégoriques des systèmes de trames, Diagrammes 18, Paris, 1987. Zbl0672.18001MR944790
  20. [Lair79] Christian Lair: Condition syntaxique de triplabilité d'un foncteur algébrique esquissé, Diagrammes 1, Paris, 1979, Zbl0511.18009MR684431
  21. [Lambek-Scott86] Joachim Lambek et Philip J. Scott: Introduction to higher order categorical logic, Cambridge Univ, Press, 1986, Zbl0596.03002MR856915
  22. [MacDonald-Stone84] John MacDonaldet Arthur Stone: Topoï over graphe, Cahiers de Topologie et Géométrie Différentielle, vol. XXV-1, Amiens, 1984. Zbl0546.18004
  23. [Pitts87] Andrew M. Pitts: Polymorphism is set-theoretic constructively, in Proceedings of Category Theory and Computer Science, edited by D. H. Pitt, A. Poigné, D.E. Rydeheard, Lect, Notes in Comp. Sci. 283, Springer, 1987. Zbl0644.18003MR925222
  24. [Reynolds84] John C. Reynolds: Polymorphism is not set-theoretic, in Semantics of Data Types, edited by G. Kahn et al. , Lect. Notes in Comp. Sci. 173, Springer, 1984, Zbl0554.03012MR784456
  25. [Seely87] R. A. G. Seely: Categorical senantics for higher order Solynorphic μ- calculus, The journal of symbolic Logic, vol. 52-4, 1987 . Zbl0642.03007MR916402

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.