Hostname: page-component-6bf8c574d5-26wn4 Total loading time: 0 Render date: 2025-02-14T12:43:33.355Z Has data issue: false hasContentIssue false
  • English
  • Français

Categorical semantics for higher order polymorphic lambda calculus

Published online by Cambridge University Press:  12 March 2014

R. A. G. Seely
R. A. G. Seely*
Affiliation:
Department of Mathematics, John Abbott College, Ste. Anne de Bellevue, Québec H9X 3L9, Canada
Get access Rights & Permissions [Opens in a new window]

Abstract

A categorical structure suitable for interpreting polymorphic lambda calculus (PLC) is defined, providing an algebraic semantics for PLC which is sound and complete. In fact, there is an equivalence between the theories and the categories. Also presented is a definitional extension of PLC including “subtypes”, for example, equality subtypes, together with a construction providing models of the extended language, and a context for Girard's extension of the Dialectica interpretation.

Type
Research Article
Information
The Journal of Symbolic Logic , Volume 52 , Issue 4 , December 1987 , pp. 969 - 989
Copyright
Copyright © Association for Symbolic Logic 1987

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

References

REFERENCES

Barendregt, H. and Rezus, A. [1983], Semantics for classical AUTOMATH and related systems, Information and Control, vol. 59, pp. 127–147.CrossRefGoogle Scholar
Bruce, K. B. and Meyer, A. R. [1984], The semantics of second order polymorphic lambda calculus, Semantics of data types (Kahn, G.et al., editors), Lecture Notes in Computer Science, vol. 173, Springer-Verlag, Berlin, pp. 131–144.CrossRefGoogle Scholar
Burstall, R., MacQueen, D. and Sannella, D. [1980], HOPE: an experimental applicative language, Report CSR-62-80, Computer Science Department, Edinburgh University, Edinburgh.Google Scholar
Freyd, P. [1972], Aspects of topoi, Bulletin of the Australian Mathematical Society, vol. 7, pp. 1–76.CrossRefGoogle Scholar
Girard, J.-Y. [1971], Une extension de l'interprétation de Gödel à l'analyse, et son application à l'élimination des coupures dans l'analyse et la théorie des types, Proceedings of the second Scandinavian logic symposium (Fenstad, J. E., editor), North-Holland, Amsterdam, pp. 63–92.CrossRefGoogle Scholar
Girard, J.-Y. [1972], Interprétation fonctionnelle et élimination des coupures de l'arithmétique d'ordre supérieur, Thèse de Doctorat d'État, Université Paris-VII, Paris. (Much of this is summarised in Girard [1971], [1973].)Google Scholar
Girard, J.-Y. [1973], Quelques résultats sur les interprétations fonctionnelles, Cambridge summer school in mathematical logic (Mathias, A. R. D. and Rogers, H., editors), Lecture Notes in Mathematics, vol. 337, Springer-Verlag, Berlin, pp. 232–252.CrossRefGoogle Scholar
Hyland, J. M. E., Johnstone, P. T. and Pitts, A. M. [1980], Tripos theory, Mathematical Proceedings of the Cambridge Philosophical Society, vol. 88, pp. 205–232.CrossRefGoogle Scholar
Lamarche, F. [1985], Unpublished lecture notes, McGill University, Montréal.Google Scholar
Lambek, J. and Scott, P. J. [1986], Introduction to higher order categorical logic, Cambridge Studies in Advanced Mathematics, vol. 7, Cambridge University Press, Cambridge.Google Scholar
Lane, S. Mac [1971], Categories for the working mathematician, Springer-Verlag, Berlin.CrossRefGoogle Scholar
McCracken, N. J. [1979], An investigation of a programming language with a polymorphic type structure, Ph.D. Thesis, Syracuse University, Syracuse, New York.Google Scholar
Milner, R. [1984], The standard ML core language, Report CSR-168-84, Computer Science Department, Edinburgh University, Edinburgh.Google Scholar
Paré, R. and Schumacher, D. [1978], Abstract families and the adjoint functor theorems, Indexed categories and their applications (Johnstone, P. T. and Paré, R., editors), Lecture Notes in Mathematics, vol. 661, Springer-Verlag, Berlin, pp. 1–125.CrossRefGoogle Scholar
Reynolds, J. C. [1974], Towards a theory of type structure, Collogue sur la programmation (Robinet, B. editor), Lecture Notes in Computer Science, vol. 19, Springer-Verlag, Berlin, pp. 408–425.Google Scholar
Reynolds, J. C. [1984], Polymorphism is not set-theoretic, Semantics of data types (Kahn, G.et al., editors), Lecture Notes in Computer Science, vol. 173, Springer-Verlag, Berlin, pp. 145–156.CrossRefGoogle Scholar
Scott, D. S. [1976], Data types as lattices, SIAM Journal on Computing, vol. 5, pp. 522–587.CrossRefGoogle Scholar
Scott, P. J. [1978], The “Dialectica” interpretation and categories, Zeitschrift für Mathematische Logik und Grundlagen der Mathematik, vol. 24, pp. 553–575.CrossRefGoogle Scholar
Seely, R. A. G. [1979], Girard's type theory and categories, Unpublished lecture notes, McGill University, Montréal.Google Scholar
Seely, R. A. G. [1982], Review of P. T. Johnstone, Topos theory, this Journal, vol. 47, pp. 448–450.Google Scholar
Seely, R. A. G. [1983], Hyperdoctrines, natural deduction and the Beck condition, Zeitschrift für Mathematische Logik und Grundlagen der Mathematik, vol. 29, pp. 505–542.CrossRefGoogle Scholar
Seely, R. A. G. [1984], Locally cartesian closed categories and type theory, Mathematical Proceedings of the Cambridge Philosophical Society, vol. 95, pp. 33–48.CrossRefGoogle Scholar
Seely, R. A. G. [1986a], Higher order polymorphic lambda calculus and categories. I, Mathematical Reports of the Academy of Science (Canada), vol. 8, pp. 135–139.Google Scholar
Seely, R. A. G. [1986b], Higher order polymorphic lambda calculus and categories. II, Mathematical Reports of the Academy of Science (Canada), vol. 8, pp. 197–201.Google Scholar