Relating models of impredicative type theories Export

@incollection{citeulike:4267922, abstract = {The object of study of this paper is the categorical semantics of three impredicative type theories, viz. Higher Order -calculus F, the Calculus of Constructions and Higher Order ML. The latter is particularly interesting because it is a two-level type theory with type dependency at both levels. Having described appropriate categorical structures for these calculi, we establish translations back and forth between all of them. Most of the research in the paper concerns the theory of fibrations and comprehension categories.}, author = {Jacobs, Bart and Moggi, Eugenio and Streicher, Thomas}, citeulike-article-id = {4267922}, citeulike-linkout-0 = {http://dx.doi.org/10.1007/BFb0013467}, citeulike-linkout-1 = {http://www.springerlink.com/content/m1060554r444h044}, citeulike-linkout-2 = {http://www.disi.unige.it/person/MoggiE/ftp/ctcs91.ps.gz}, doi = {10.1007/BFb0013467}, journal = {Category Theory and Computer Science}, keywords = {category-theory, type-theory}, pages = {197--218}, posted-at = {2009-04-03 05:08:53}, priority = {2}, title = {Relating models of impredicative type theories}, url = {http://dx.doi.org/10.1007/BFb0013467}, year = {1991} }

TY - CHAP ID - citeulike:4267922 L3 - citeulike-article-id:4267922 N2 - The object of study of this paper is the categorical semantics of three impredicative type theories, viz. Higher Order -calculus F, the Calculus of Constructions and Higher Order ML. The latter is particularly interesting because it is a two-level type theory with type dependency at both levels. Having described appropriate categorical structures for these calculi, we establish translations back and forth between all of them. Most of the research in the paper concerns the theory of fibrations and comprehension categories. JF - Category Theory and Computer Science EP - 218 TI - Relating models of impredicative type theories SP - 197 KW - category-theory KW - type-theory AU - Jacobs, Bart AU - Moggi, Eugenio AU - Streicher, Thomas PY - 1991/// UR - http://dx.doi.org/10.1007/BFb0013467 ER -