×

Semantique catégorique des constructeurs de types d’ordre supérieur. (Categorical semantics of constructors of polymorphic types). (French) Zbl 0703.18003

Summary: We describe a new categorical framework for the semantics of polymorphic type theory. Its two main features are: variable types are mere maps rather than functors; the type \(\forall X.A(X)\) is the solution of a small inductive universal problem instead that of a big projective one. For this purpose, we introduce abstract “type syntaxes”, in the spirit of Ehresmann’s sketches, and study their semantics. We get a quite general result of algebraicity (tripleability).

MSC:

18C10 Theories (e.g., algebraic theories), structure, and semantics
18C15 Monads (= standard construction, triple or triad), algebras for monads, homology and derived functors for monads
03G30 Categorical logic, topoi
PDFBibTeX XMLCite
Full Text: EuDML

References:

[1] J.-Y. Girard, Proofs and types, Cambridge University Press, 1989 (version originale française dactylographiée sous le titre Lambda-calcul typé) Zbl0671.68002 MR1003608 · Zbl 0671.68002
[2] P.J. Freyd, Structural polymorphism, draft (23 jan. 89)
[3] P. Ageron, Sémantique catégorique des types : comprendre le système F, Diagrammes 19, 1988 Zbl0672.03049 MR976067 · Zbl 0672.03049
[4] C. Lair, Trames et sémantiques catégoriques des systèmes de trames, Diagrammes 18, 1987 Zbl0672.18001 MR944790 · Zbl 0672.18001
[5] P. Ageron, Logiques, catégories et esquisses, thèse de doctorat, à soutenir
[6] L. Coppey et C. Lair, Leçons de théorie des esquisses (I) Diagrammes 12, 1984 et (II) Diagrammes 19, 1988 Zbl0562.18002 MR800501 · Zbl 0562.18002
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.