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.
Preview
Unable to display preview. Download preview PDF.
References
Cartmell, J. [1978] Generalised Algebraic Theories and Contextual Categories, Ph.D. thesis, Univ. Oxford.
Coquand, T. and Huet G. [1988] The Calculus of Constructions, in: Information and Computation (1988), vol. 73, num. 2/3.
Ehrhard, Th. [1988] A Categorical Semantics of Constructions, in: Logic in Computer Science (Computer Society Press, Washington, 1988) 264–273.
Hyland, J.M.E. and Pitts, A.M. [1989] The Theory of Constructions: categorical semantics and topos-theoretic Models, in: Gray, J. and Scedrov, A., (eds.), Categories in Computer Science and Logic (Contemp. Math. 92, AMS, Providence, 1989).
Jacobs, B.P.F. [1990] Comprehension Categories and the Semantics of Type Dependency, manuscript.
[1991] Categorical Type Theory, Ph.D. thesis, Univ. Nijmegen.
Moggi, E. [1991] A Category Theoretic Account of Program Modules, Math. Struct. in Comp. Sc. (1991), vol. 1.
Pavlović, D. [1990] Predicates and Fibrations, Ph.D. thesis, Univ. Utrecht.
Pitts, A.M. [1989] Categorical Semantics of Dependent Types, Notes of a talk given at SRI Menlo Park and at the Logic Colloquium in Berlin.
Seely, R.A.G. [1984] Locally cartesian closed Categories and Type Theory, Math. Proc. Camb. Phil. Soc.95 33–48.
[1987] Categorical Semantics for higher order Polymorphic Lambda Calculus, J. Symb. Log. 52 969–989.
Streicher, Th. [1989] Correctness and Completeness of a Categorical Semantics of the Calculus of Constructions, Ph.D. thesis, Univ. Passau.
Taylor, P. [1987] Recursive Domains, indexed Categories and Polymorphism, Ph.D. thesis, Univ. Cambridge.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1991 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Jacobs, B., Moggi, E., Streicher, T. (1991). Relating models of impredicative type theories. In: Pitt, D.H., Curien, PL., Abramsky, S., Pitts, A.M., Poigné, A., Rydeheard, D.E. (eds) Category Theory and Computer Science. CTCS 1991. Lecture Notes in Computer Science, vol 530. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0013467
Download citation
DOI: https://doi.org/10.1007/BFb0013467
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-54495-1
Online ISBN: 978-3-540-38413-7
eBook Packages: Springer Book Archive