Abstract
There are compelling benefits to using foundational type theory as a framework for programming language semantics. I give a semantics of an expressive programming calculus in the foundational type theory of Nuprl. Previous type-theoretic semantics have used less expressive type theories, or have sacrificed important programming constructs such as recursion and modules. The primary mechanisms of this semantics are partial types, for typing recursion, set types, for encoding power and singleton kinds, which are used for subtyping and module programming, and very dependent function types,for encoding signatures.
Chapter PDF
Similar content being viewed by others
References
Allen, S. (1987) A non-type-theoretic definition of Martin-Löf’s types. In Second IEEE Symposium on Logic in Computer Science, pages 215–221, Ithaca, New York.
Birkedal, L. and Harper, R. (1997) Relational interpretations of recursive types in an operational setting. In Theoretical Aspects of Computer Software.
Constable, R., Allen, S., Bromley, H., Cleaveland, W., Cremer, J., Harper, R., Howe, D., Knoblock, T., Mendler, N., Panangaden, P., Sasaki, J., and Smith, S. (1986) Implementing Mathematics with the Nuprl Proof Development System. Prentice-Hall.
Constable, R. L. (1985) Constructive mathematics as a programming logic I: Some principles of theory. In Topics in the Theory of Computation, volume 24 of Annals of Discrete Mathematics, pages 21–37. Elsevier. Selected papers of the International Conference on Foundations of Computation Theory 1983.
Constable, R. L. (1991) Type theory as a foundation for computer science. In Theoretical Aspects of Computer Software 1991, volume 526 of Lecture Notes in Computer Science, pages 226–243, Sendai, Japan. Springer-Verlag.
Constable, R. L. and Crary, K. (1997) Computational complexity and induction for partial computable functions in type theory. Technical report, Department of Computer Science, Cornell University.
Constable, R. L. and Smith, S. F. (1987) Partial objects in constructive type theory. In Second IEEE Symposium on Logic in Computer Science, pages 183–193, Ithaca, New York.
Coquand, T. and Huet, G. (1988) The calculus of constructions. Information and Computation, 76: 95–120.
Crary, K. (1997) Foundations for the implementation of higher-order subtyping. In 1997 ACM SIGPLAN International Conference on Functional Programming,pages 125–135, Amsterdam.
Crary, K. (1998a) Admissibility of fixpoint induction over partial types. Technical report, Department of Computer Science, Cornell University.
Crary, K. (1998b) Programming language semantics in foundational type theory. Technical Report TR98–1666, Department of Computer Science, Cornell University.
Crary, K. (1998c) Type-Theoretic Methodology for Practical Programming Languages. PhD thesis, Department of Computer Science, Cornell University, Ithaca, New York. Forthcoming.
Girard, J.-Y. (1972) Interprétation fonctionelle et élimination des coupures de l’arithmétique d’ordre supérieur. PhD thesis, Université Paris V II.
Harper, R. (1992) Constructing type systems over an operational semantics. Journal of Symbolic Computation, 14: 71–84.
Harper, R. and Lillibridge, M. (1994) A type-theoretic approach to higher-order modules with sharing. In Twenty-First ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, pages 123–137, Portland, Oregon.
Harper, R. and Mitchell, J. C. (1993) On the type structure of Standard ML. ACM Transactions on Programming Languages and Systems, 15 (2): 211–252.
Harper, R., Mitchell, J. C., and Moggi, E. (1990) Higher-order modules and the phase distinction. In Seventeenth ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages,pages 341–354, San Francisco.
Harper, R. and Stone, C. (1998) A type-theoretic interpretation of Standard ML. In Proof, Language and Interaction: Essays in Honour of Robin Milner. The MIT Press. To appear.
Hickey, J. J. (1996) Formal objects in type theory using very dependent types. In Foundations of Object Oriented Languages 3.
Howard, W. (1980) The formulas-as-types notion of construction. In Seldin, J. P. and Hindley, J. R., editors, To H.B. Curry: Essays on Combinatory Logic, Lambda-Calculus and Formalism,pages 479–490. Academic Press.
Howe, D. J. (1996) Semantic foundations for embedding HOL in Nuprl. Technical report, Bell Labs.
Kreitz, C. (1997) Formal reasoning about communications systems I. Technical report, Department of Computer Science, Cornell University.
Martin-Löf, P. (1982) Constructive mathematics and computer programming In Sixth International Congress of Logic, Methodology and Philosophy of Science,volume 104 of Studies in Logic and the Foundations of Mathematics,pages 153175. North-Holland.
Mendier, P. F. (1987) Inductive Definition in Type Theory. PhD thesis, Department of Computer Science, Cornell University, Ithaca, New York.
Milner, R., Tofte, M., Harper, R., and MacQueen, D. (1997) The Definition of Standard ML (Revised). The MIT Press, Cambridge, Massachusetts.
Palmgren, E. and Stoltenberg-Hansen, V. (1989) Domain interpretations of intuitionistic type theory. U.U.D.M. Report 1989:1, Uppsala University, Department of Mathematics.
Peyton Jones, S. L. and Wadler, P. (1993) Imperative functional programming. In Twentieth ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages,Charleston, South Carolina.
Reynolds, J. C. (1981) The essence of Algol. In de Bakker, J. W. and van Vliet, J. C., editors, Proceedings of the International Symposium on Algorithmic Languages, pages 345–372, Amsterdam. North-Holland.
Rezus, A. (1985) Semantics of constructive type theory. Technical Report 70, Infor- matics Department, Faculty of Science, Nijmegen, University, The Netherlands.
Scott, D. and Strachey, C. (1971) Toward a mathematical semantics for computer languages. In Proceedings of the Symposium on Computers and Automata,volume 21 of Microwave Research Institute Symposia Series. Polytechnic Institute of Brooklyn.
Smith, S. F. (1989) Partial Objects in Type Theory. PhD thesis, Department of Computer Science, Cornell University, Ithaca, New York.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1998 Springer Science+Business Media Dordrecht
About this chapter
Cite this chapter
Crary, K. (1998). Programming Language Semantics in Foundational Type Theory. In: Gries, D., de Roever, WP. (eds) Programming Concepts and Methods PROCOMET ’98. IFIP — The International Federation for Information Processing. Springer, Boston, MA. https://doi.org/10.1007/978-0-387-35358-6_11
Download citation
DOI: https://doi.org/10.1007/978-0-387-35358-6_11
Publisher Name: Springer, Boston, MA
Print ISBN: 978-1-4757-6299-0
Online ISBN: 978-0-387-35358-6
eBook Packages: Springer Book Archive