Abstract
In this paper we discuss Martin-Löf's partial type theory, that is type theory with general recursion, and in particular the consequences of the presence of a fixed point operator. We model Martin-Löf's logical framework domain-theoretically in the category of conditional upper semi lattices and parametrizations thereof. An interpretation of a type of sets in the logical framework, which defines partial type theory with one universe, is finally described.
This is a preview of subscription content, log in via an institution to check access.
Similar content being viewed by others
References
Constable, R. and N. P. Mendler,Recursive definitions in type theory, in:Logics of Programs, Brooklyn 1985, (ed. R. Parikh), Springer Lecture Notes in Computer Science vol. 193, Springer, 1985.
Dybjer, P.,Inductively defined sets in Martin-Löf's set theory, manuscript, 1988.
Griffor, E. R., I. Lindström and V. Stoltenberg-Hansen,Mathematical Theory of Domains, Cambridge University Press, to appear.
Martin-Löf, P.,An intuitionistic theory of types: predicative part, in:Logic Colloquium '73, (eds. E. H. Rose, J. C. Shepherdson), North-Holland, 1975, pp. 73–118.
Martin-Löf, P.,Constructive mathematics and computer programming, in:Logic, Methodology and Philosophy of Science VI (eds. L. J. Cohen, et al.), North-Holland, 1982, pp. 153–175.
Martin-Löf, P.,The domain interpretation of type theory, in:Workshop on Semantics of Programming Languages, Abstracts and Notes (eds. K. Karlsson and K. Petterson), Programing Methodology Group, Chalmer's University of Technology and University of Göteborg, 1983.
Martin-Löf, P.,Mathematics of infinity, in: Proceedings of the COLOG 88 conference, Tallinn (eds. P. Martin-Löf and G. E. Mints), Springer Lecture Notes in Computer Science, Springer 1989.
Nordström, B., K. Petterson and J. M. Smith,Programming in Martin-Löf's Type Theory. An Introduction, Oxford University Press, 1990.
Palmgren, E. and V. Stoltenberg-Hansen,Domain interpretations of Martin-Löf's partial type theory, Annals of Pure and Applied Logic 48 (1990), pp. 135–196.
Palmgren, E.,An information system interpretation of Martin-Löf's partial type theory with universes, Information and Computation, to appear.
Palmgren, E.,A construction of Type: Type in Martin-Löf's partial type theory with one universe, Journal of Symbolic Logic, to appear.
Palmgren, E. and V. Stoltenberg-Hansen,Martin-Löf's partial type theory, U.U.D.M. Report 1990: 3, Uppsala, 1990.
Smith, J. M.,The independence of Peano's fourth axiom from Martin-Löf's type theory without universes, Journal of Symbolic Logic 53 (1988), pp. 840–845.
Author information
Authors and Affiliations
Additional information
During the preparation of this paper, the first author was supported by the Swedish Natural Science Research Council as a PhD-student in mathematical logic.
Rights and permissions
About this article
Cite this article
Palmgren, E., Stoltenberg-Hansen, V. Remarks on Martin-Löf's partial type theory. BIT 32, 70–83 (1992). https://doi.org/10.1007/BF01995109
Received:
Revised:
Issue Date:
DOI: https://doi.org/10.1007/BF01995109