Types, abstraction, and parametric polymorphism, part 2

1. Reynolds, J. C. Types, Abstraction and Parametric Polymorphism, in: Information Processing 83, Proceedings of the IFIP 9th World Computer Congress, Paris, September 19–23, 1983, edited by R. E. A. Mason. Elsevier Science Publishers B. V. (North-Holland), Amsterdam, 1983, pp. 513–523.

   Google Scholar 

2. Girard, J.-Y. Une Extension de l'Interprétation de Gödel à l'Analyse, et son Application à l'Elimination des Coupures dans l'Analyse et la Théorie des Types, in: Proceedings of the Second Scandinavian Logic Symposium, University of Oslo, June 18–20, 1970, edited by J. E. Fenstad. Studies in Logic and the Foundations of Mathematics, vol. 63, North-Holland, Amsterdam, 1971, pp. 63–92.

   Google Scholar 

3. Girard, J.-Y. Interprétation Fonctionnelle et Elimination des Coupures de l'Arithmétique d'Ordre Supérieur, Thèse de doctorat d'état. Université Paris VII, June 1972.

   Google Scholar 

4. Reynolds, J. C. Towards a Theory of Type Structure, in: Programming Symposium, Proceedings, Colloque sur la Programmation, Paris, April 9–11, edited by B. Robinet. Lecture Notes in Computer Science, vol. 19, Springer-Verlag, Berlin, 1974, pp. 408–425.

   Google Scholar 

5. Strachey, C. Fundamental Concepts in Programming Languages. Unpublished lecture notes, International Summer School in Computer Programming, Copenhagen, August 1967.

   Google Scholar 

6. Plotkin, G. D. Lambda-Definability and Logical Relations. Memorandum, no. SAI-RM-4, University of Edinburgh, School of Artificial Intelligence, October 1973.

   Google Scholar 

7. Reynolds, J. C. Polymorphism is not Set-Theoretic. in: Semantics of Data Types, International Symposium, Sophia-Antipolis, France, June 27–29, edited by G. Kahn, D. B. MacQueen, and G. D. Plotkin. Lecture Notes in Computer Science, vol. 173, Springer-Verlag, Berlin, 1984, pp. 145–156.

   Google Scholar 

8. Reynolds, J. C. and Plotkin, G. D. On Functors Expressible in the Polymorphic Typed Lambda Calculus. Report, no. CMU-CS-90-147, Carnegie Mellon University, School of Computer Science, July 6, 1990. Also to appear in Information and Computation.

   Google Scholar 

9. Seely, R. A. G. Categorical Semantics for Higher Order Polymorphic Lambda Calculus. Journal of Symbolic Logic, vol. 52 (1987), pp. 969–989.

   Google Scholar 

10. Pitts, A. M. Polymorphism is Set Theoretic, Constructively, in: Category Theory and Computer Science, Edinburgh, Scotland, September 7–9, edited by D. H. Pitt, A. Poigné, and D. E. Rydeheard. Lecture Notes in Computer Science, vol. 283, Springer-Verlag, Berlin, 1987.

    Google Scholar 

11. Narayanan, B. R. A General Framework for Models of Type Polymorphism, Ph. D. Dissertation. Syracuse University, December 1988, vi+155 pp. Report No. CIS-89-1.

    Google Scholar 

12. Lambek, J. and Scott, P. J. Introduction to Higher Order Categorical Logic. Cambridge Studies in Advanced Mathematics, vol. 7, Cambridge University Press, Cambridge, England, 1986, ix+293 pp.

    Google Scholar 

13. Barr, M. and Wells, C. Toposes, Triples, and Theories. Grundlehren der mathematischen Wissenschaften, vol. 278, Springer-Verlag, New York, 1985, xiii+345 pp.

    Google Scholar 

14. Lawvere, F. W. Functorial Semantics of Algebraic Theories. Proceedings of the National Academy of Sciences of the United States of America, vol. 50 (1963), pp. 869–872.

    Google Scholar 

15. Lawvere, F. W. Some Algebraic Problems in the Context of Functorial Semantics of Algebraic Theories. in: Reports of the Midwest Category Seminar II, edited by S. Mac Lane. Lecture Notes in Mathematics, vol. 61, Springer-Verlag, Berlin, 1968, pp. 41–61.

    Google Scholar 

16. Mac Lane, S. Categories for the Working Mathematician. Graduate Texts in Mathematics, vol. 5, Springer-Verlag, New York, 1971, ix+262 pp.

    Google Scholar 

17. Milner, R. A Theory of Type Polymorphism in Programming. Journal of Computer and System Sciences, vol. 17 (1978), pp. 348–375.

    Article  Google Scholar 

18. Damas, L. and Milner, R. Principal Type-Schemes for Functional Programs. in: Conference Record of the Ninth Annual ACM Symposium on Principles of Programming Languages, Albuquerque, New Mexico, January 25–27. 1982, pp. 207–212.

    Google Scholar 

19. Harper, R. and Mitchell, J. C. On the Type Structure of Standard ML. ACM Transactions on Programming Languages and Systems, To appear.

    Google Scholar 

20. Plotkin, G. D. Lambda-Definability in the Full Type Hierarchy, in: To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, edited by J. P. Seldin and J. R. Hindley. Academic Press, London, 1980, pp. 363–373.

    Google Scholar 

21. McCracken, N. J. An Investigation of a Programming Language with a Polymorphic Type Structure, Ph. D. Dissertation. Syracuse University, June 1979, iv+126 pp.

    Google Scholar 

22. McCracken, N. J. A Finitary Retract Model for the Polymorphic Lambda-Calculus. Unpublished, Syracuse University, 1982.

    Google Scholar 

23. Amadio, R., Bruce, K. B., and Longo, G. The Finitary Projection Model for Second Order Lambda Calculus and Solutions to Higher Order Domain Equations, in: Proceedings Symposium on Logic in Computer Science, Cambridge, Massachusetts, June 16–18. 1986, pp. 122–130.

    Google Scholar 

24. Girard, J.-Y. The System F of Variable Types, Fifteen Years Later. Theoretical Computer Science, vol. 45 (1986), pp. 159–192.

    Google Scholar 

25. Coquand, T., Gunter, C. A., and Winskel, G. DI-Domains as a Model of Polymorphism. in: Mathematical Foundations of Programming Language Semantics, 3rd Workshop, Tulane University, New Orleans, April 8–10, 1987, edited by M. Main, A. Melton, M. Mislove, and D. A. Schmidt. Lecture Notes in Computer Science, vol. 298, Springer-Verlag, Berlin, 1988, pp. 344–363.

    Google Scholar 

26. Coquand, T., Gunter, C. A., and Winskel, G. Domain Theoretic Models of Polymorphism. Information and Computation, vol. 81 (1989), pp. 123–167.

    Google Scholar 

27. Howard, W. A. Hereditarily Majorizable Functionals of Finite Type. in: Metamathematical Investigation of Intuitionistic Arithmetic and Analysis, edited by A. S. Troelstra. Lecture Notes in Mathematics, vol. 344, Springer-Verlag, Berlin, 1973, pp. 454–461. Appendix.

    Google Scholar 

28. Statman, R. Logical Relations and the Typed λ-Calculus. Information and Control, vol. 65 (1985), pp. 85–97.

    Google Scholar 

29. Mitchell, J. C. and Meyer, A. R. Second-order Logical Relations (Extended Abstract). in: Logic of Programs, Brooklyn, New York, June 17–19, edited by R. Parikh. Lecture Notes in Computer Science, vol. 193, Springer-Verlag, Berlin, 1985, pp. 225–236.

    Google Scholar 

30. Bruce, K. B., Meyer, A. R., and Mitchell, J. C. The Semantics of Second-Order Lambda Calculus. Information and Computation, vol. 85 (1990), pp. 76–134.

    Google Scholar 

31. Jacobs, B. P. F. On the Semantics of Second Order Lambda Calculus: From BruceMeyer-Mitchell Models to Hyperdoctrine Models and Vice-Versa. in: Category Theory and Computer Science, Manchester, UK, September 5–8, edited by D. H. Pitt, D. E. Rydeheard, P. Dybjer, A. M. Pitts, and A. Poigné. Lecture Notes in Computer Science, vol. 389, Springer-Verlag, Berlin, 1989, pp. 198–212.

    Google Scholar 

32. Jacobs, B. P. F. Semantics of the second order Lambda Calculus. Mathematical Structures in Computer Science, To appear.

    Google Scholar 

33. Wadler, P. Theorems for Free. in: Functional Programming Languages and Computer Architecture, FPCA '89 Conference Proceedings Fourth International Conference, Imperial College, London, September 11–13. ACM, 1989, pp. 347–359.

    Google Scholar 

34. Hasegawa, R. Categorical Data Types in Parametric Polymorphism. Unpublished, November 16, 1990.

    Google Scholar 

35. Freyd, P. J. and Scedrov, A. Categories, Allegories. North-Holland Mathematical Library, vol. 39, North-Holland, Amsterdam, 1990, xviii+296 pp.

    Google Scholar 

36. Mitchell, J. C. and Scedrov, A. Sconing, Relators, and Parametricity. Unpublished draft, October 21, 1991.

    Google Scholar 

37. Bainbridge, E. S., Freyd, P. J., Scedrov, A., and Scott, P. J. Functorial Polymorphism. Theoretical Computer Science, vol. 70 (1990), pp. 35–64. Corrigendum in (3) 71, 10 April 1990, p. 431.

    Article  Google Scholar 

38. Girard, J.-Y., Scedrov, A., and Scott, P. J. Normal Forms and Cut-Free Proofs as Natural Transformations. in: Logic from Computer Science, A Mathematical Sciences Research Institute Workshop, Berkeley, California, November 1989, edited by Y. N. Moschovakis. MSRI Series, vol. 21, Springer-Verlag, 1991, pp. 217–241.

    Google Scholar 

39. Freyd, P. J. Structural Polymorphism. Unpublished, January 23, 1989.

    Google Scholar 

40. Kelly, G. M. Private communication. July 1991.

    Google Scholar 

41. Abramsky, S. and Jensen, T. P. A Relational Approach to Strictness Analysis for Higher-Order Polymorphic Functions. in: Conference Record of the Eighteenth Annual ACM Symposium on Principles of Programming Languages, Orlando, Florida, January 21–23. 1991, pp. 49–54.

    Google Scholar 

42. Böhm, C. and Berarducci, A. Automatic Synthesis of Typed λ-Programs on Term Algebras. Theoretical Computer Science, vol. 39 (1985), pp. 135–154.

    Article  Google Scholar 

43. Leivant, D. Reasoning About Functional Programs and Complexity Classes Associated with Type Disciplines. in: 24th Annual Symposium on Foundations of Computer Science, IEEE, Tucson, Arizona, November 7–9. 1983, pp. 460–469.

    Google Scholar 

44. Martin-Löf, P. A Construction of the Provable Wellorderings of the Theory of Species. Unpublished.

    Google Scholar 

45. Freyd, P. J. POLYNAT in PER. in: Categories in Computer Science and Logic, Boulder, Colorado, June 14–20,1987, edited by J. W. Gray and A. Scedrov. Contemporary Mathematics, vol. 92, American Mathematical Society, Providence, Rhode Island, 1989, pp. 67–68.

    Google Scholar 

Download references