Parametric polymorphism (parametricity; inference; checking; models)

Academic Journals

1. J. Roger Hindley. M. H. Newman's Typability Algorithm for Lambda-calculus. J. Log. Comput, 18(2):229-238, 2008.
2. Andy Pitts. Parametric Polymorphism and Operational Equivalence. Mathematical Structures in Computer Science, 10:321-359, 2000.
3. Fritz Henglein. Breaking Through the $n^3$ Barrier: Faster Object Type Inference. Theory and Practice of Object Systems (TAPOS), Invited paper selected from 4th Int'l Workshop on Foundations of Object-Oriented Languages (FOOL), January 1997, Paris, France, 5(1):57-72, 1999.
4. Pawel Urzyczyn. Type Reconstruction in F$_\omega$. Mathematical Structures in Computer Science (MSCS), 7:329-358, 1997.
5. Andrew M. Pitts. Relational Properties of Domains. Information and Computation, 127(2):66-90, June 1996.
6. Konstantin L\"aufer. Type classes with existential types. Journal of Functional Programming (JFP), 6(3):485-517, May 1996.
7. Mark Jones. A Theory of Qualified Types. Science of Computer Programming, 22:231-256, 1994.
8. Geoffrey S. Smith. Principal type schemes for functional programs with overloading and subtyping. Science of Computer Programming, 23:197-226, 1994.
9. Fritz Henglein, Harry Mairson. The Complexity of Type Inference for Higher-Order Typed Lambda Calculi. Journal of Functional Programming (JFP), 4(4):435-477, October 1994.
10. Robert Harper, John Mitchell. On the Type Structure of Standard ML. ACM Transactions on Programming Languages and Systems (TOPLAS), Based on paper presented at POPL '88, 15(2):211-252, April 1993.
11. Fritz Henglein. Type Inference with Polymorphic Recursion. ACM Transactions on Programming Languages and Systems (TOPLAS), 15(2):253-289, April 1993. download
12. Andrew Chi-Chih Yao. Lower Bounds for Algebraic Computation Trees with Integer Inputs. SIAM J. Comput, 20(4):655-668, 1991.
13. D. Leivant. Finitely Stratified Polymorphism. Information and Computation, Presented at LICS '89, 93(1):93-113, July 1991.
14. J. Mitchell. Type Inference with Simple Subtypes. J. Functional Programming, 1(3):245-285, July 1991.
15. M. Wand. Type Inference for Record Concatenation and Multiple Inheritance. Information and Computation, Presented at LICS '89, 93(1):1-15, July 1991.
16. Y. Fuh, P. Mishra. Type Inference with Subtypes. Theoretical Computer Science (TCS), 73:155-175, 1990.
17. M. Tofte. Type Inference for Polymorphic References. Information and Computation, 89(1):1-34, November 1990.
18. J. Mitchell. Polymorphic Type Inference and Containment. Information and Control, 76:211-249, 1988.
19. J. Mitchell, G. Plotkin. Abstract Types have Existential Types. ACM Trans. on Programming Languages and Systems, 10(3):470-502, 1988.
20. S. Ronchi Della Rocca. Principal Type Scheme and Unification for Intersection Type Discipline. Theoretical Computer Science, 59:181-209, 1988.
21. L. Cardelli. Basic Polymorphic Type Checking. Science of Computer Programming, 8:147-172, 1987.
22. M. Wand. A Simple Algorithm and Proof for Type Inference. Fundamenta Informaticae, X:115-122, 1987.
23. R. Statman. Logical Relations and the Typed Lambda Calculus. Information and Control, 65:85-97, 1985.
24. L. Cardelli, P. Wegner. On Understanding Types, Data Abstraction and Polymorphism. ACM Computing Surveys, 17(4):471-522, December 1985.
25. L. Cardelli. Basic Polymorphic Typechecking. Polymorphism, 2(1), January 1985.
26. A. Mycroft, R. O'Keefe. A Polymorphic Type System for PROLOG. Artificial Intelligence, 23:295-307, 1984.
27. R. Hindley. The Completeness Theorem for Typing Lambda-Terms. Theoretical Computer Science, 22:1-17, 1983.
28. R. Hindley. Curry's Type-Rules are Complete with Respect to the F-Semantics too. Theoretical Computer Science, 22:127-133, 1983.
29. J. Reynolds. Types, Abstraction and Parametric Polymorphism. Information Processing, pages 513-523, 1983.
30. M. Coppo, M. Dezani-Ciancaglini. A New Type Assignment for Lambda-Terms. Archive f. math. Logik und Grundlagenforschung, 19:139-156, 1979.
31. R. Statman. The Typed Lambda Calculus is not Elementary Recursive. Theoretical Computer Science, 9:73-82, 1979.
32. Nicholas Pippenger, Michael J. Fischer. Relations Among Complexity Measures. J. ACM, 26(2):361-381, 1979. download
33. R. Milner. A Theory of Type Polymorphism in Programming. J. Computer and System Sciences, 17:348-375, 1978.
34. R. Hindley. The Principal Type-Scheme of an Object in Combinatory Logic. Trans. Amer. Math. Soc, 146:29-60, December 1969.

Book Chapters

1. Sian Jha, Jens Palsberg, Tian Zhao, Fritz Henglein. Efficient Type Matching. In Automatic Program Development-A Tribute to Robert Paige, Springer Netherlands, 2008.
2. Didier Rémy. Type Inference for Records in a Natural Extension of ML. In Theoretical Aspects of Object-Oriented Programming, Also available as Research Report 1431, May 1991, INRIA-Rocquencourt, France. Previous results presented at POPL '89, Carl A. Gunter, John C. Mitchell (eds.), Also available as Research Report 1431, May 1991, INRIA-Rocquencourt, France. Previous results presented at POPL '89, pp. 67-95, MIT Press, 1994.
3. P. Kanellakis, H. Mairson, J. Mitchell. Unification and ML Type Reconstruction. In Computational Logic - Essays in Honor of Alan Robinson, J.-L. Lassez, G. Plotkin (eds.), MIT Press, 1991.
4. Felice Cardone, Mario Coppo. Two Extensions of Curry's Type Inference System. In Logic and Computer Science, pp. 19-75, Academic Press Ltd, 1990.
5. P. Atzeni, S. Parker. Algorithms for Set Containment Inference. F. Bancilhon, P. Buneman (eds.), Chap. 7, pp. 117-127, Frontier Series, Addison-Wesley, ACM Press, 1990.
6. P. Hancock. Polymorphic Type Checking. In The Implementation of Functional Programming Languages, S. Peyton-Jones (ed.), Chap. 8, Prentice-Hall, 1987.
7. J. Reynolds. Three Approaches to Type Structure. In Proc. TAPSOFT, pp. 97-138, LNCS, Springer-Verlag, 1985.
8. M. Coppo, M. Dezani-Ciancaglini, B. Venneri. Prinicipal Type Schemes and Lambda-Calculus Semantics. In To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, J. Seldin, J. Hindley (eds.), pp. 535-560, Academic Press, 1980.
9. G. Pottinger. A Type Assignment for the Strongly Normalizable Lambda-Terms. In To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, J. Hindley, J. Seldin (eds.), pp. 561-577, Academic Press, 1980.
10. J. Reynolds. Towards a Theory of Type Structure. In Proc. Programming Symposium, Vol. 19, pp. 408-425, LNCS, Springer-Verlag, 1974.

International Conferences

1. Mark P. Jones. Polymorphism and page tables: systems programming from a functional programmer's perspective. In ICFP '08: Proceeding of the 13th ACM SIGPLAN international conference on Functional programming, Pages 265-266, New York, NY, USA, 2008. download
2. Derek Dreyer, Robert Harper, Manuel M. T. Chakravarty, Gabriele Keller. Modular type classes. In POPL '07: Proceedings of the 34th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages, Pages 63-70, New York, NY, USA, 2007.
3. Lajos Nagy, Ryan Stansifer. Polymorphic type inference for the relational algebra in the functional database programming language neon. In ACM-SE 44: Proceedings of the 44th annual Southeast regional conference, Pages 673-678, New York, NY, USA, 2006. download
4. Patricia Johann, Janis Voigtl\"ander. Free Theorems in the Presence of seq. In Proceedings 31st Symposium on Principles of Programming Languages (POPL), Venice, Italy, 2004.
5. Aleksy Schubert. Second-Order Unification and Type Inference for Church-Style Polymorphism. In POPL, Pages 279-288, 1998. download
6. Fritz Henglein. Breaking through the $n^3$ barrier: Faster object type inference. In Proc.\ 4th Int'l Workshop on Foundations of Object-Oriented Languages (FOOL), Paris, France, Benjamin Pierce (ed.), Also DIKU TOPPS Report D-317, January 1997.
7. Jakob Rehof. Minimal typings in atomic subtyping. In Proc.\ 24th ACM SIGPLAN-SIGACT Symposium on Principles of Programmin gLanguages (POPL), Paris, France, Pages 278-291, January 1997.
8. Martin Sulzmann, Martin Odersky, Martin Wehr. Type Inference with constrained types. In Proc.\ 4th Int'l Workshop on Foundations of Object-Oriented Languages (FOOL), Paris, France, Benjamin Pierce (ed.), Published electronically at \texttthttp://www.cs.williams.edu/\\ kim/FOOL/, January 1997.
9. Fran\ccois Pottier. Simplifying Subtyping Constraints. In Proc.\ Int'l Conf. on Functional Programming (ICFP), Philadelphia, Pennsylvania, Pages 122-133, May 1996.
10. Trevor Jim. What Are Principal Typings and What Are They Cood For?. In Proc. 23rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), St. Petersburg Beach, Florida, Pages 42-53, January 1996.
11. Martin Odersky, Konstantin Läufer. Putting Type Annotations to Work. In Conference Record of POPL '96: The 23rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, St. Petersberg Beach, Florida, Pages 54-67, New York, N.Y, January 1996.
12. Jonathan Eifrig, Scott Smith, Valery Trifonov. Sound Polymorphic Type Inference for Objects. In Proc.\ 10th Annual Conf.\ on Object-Oriented Programming Systems, Languages, and Applications (OOPSLA), Austin, Texas, ACM SIGPLAN Notices, Vol. 30, Pages 169-184, October 1995.
13. Dirk Dussart, Fritz Henglein, Christian Mossin. Polymorphic Recursion and Subtype Qualifications: Polymorphic Binding-Time Analysis in Polynomial Time. In Proc.\ 2nd Int'l Static Analysis Symposium (SAS), Glasgow, Scotland, Lecture Notes in Computer Science, Pages 118-135, September 1995.
14. Valery Trifonov, Scott Smith. Subtying Constrained Types. In Proc.\ 3rd Int'l Static Analysis Symposium (SAS), Aachen, Germany, Radhia Cousot, David A. Schmidt (eds.), Lecture Notes in Computer Science (LNCS), Volume 1145, Pages 349-365, September 1995.
15. Fritz Henglein, Jakob Rehof. Safe polymorphic type inference for a dynamically typed language: Translating Scheme to ML. In FPCA '95: Proceedings of the seventh international conference on Functional programming languages and computer architecture, Pages 192-203, New York, NY, USA, June 1995. download
16. Mark P. Jones. Simplifying and Improving Qualified Types. In Proc.\ Conf. on Functional Programming Languages and Computer Architecture (FPCA), La Jolla, California, June 1995.
17. Mikael Rittri. Dimension Inference under Polymorphic Recursion. In Proc. ACM Conf.\ on Functional Programming Languages and Computer Architecture (FPCA), La Jolla, California, Pages 147-159, June 1995.
18. Jonathan Eifrig, Scott Smith, Valery Trifonov. Type Inference for Recursively Constrained Types and its Application to OOP. In Proc. 11th Conf. on the Mathematical Foundations of Programming Semantics (MFPS), April 1995.
19. Robert Harper, Greg Morrisett. Compiling Polymorphism Using Intensional Type Analysis. In Proc. ACM SIGACT/SIGPLAN Symp. on Principles of Programming Languages (POPL), San Francisco, California, January 1995.
20. My Hoang, John C. Mitchell. Lower Bounds on Type Inference with Subtypes. In Proc. 22nd ACM Symp. on Principles of Programming Languages (POPL), San Francisco, California, Pages 176-185, January 1995.
21. A. J. Kfoury, J. B. Wells. A Direct Algorithm for Type Inference in the Rank-2 Fragment of the Second-Order lambda-Calculus. In LISP and Functional Programming, Pages 196-207, 1994. download
22. Mark P. Jones. ML Typing, Explicit Polymorphism, and Qualified Types. In Proc. Conf. on Theoretical Aspects of Computer Science (TACS), Sendai, Japan, Lecture Notes in Computer Science, Vol. 789, Pages 56-75, 1994.
23. Dinesh Katiyar, David Luckham, John Mitchell, Sigurd. Polymorphism and Subtyping in Interfaces. In Proc. Workshop on Interface Definition Languages, ACM SIGPLAN Notices, Volume 29, Pages 22-34, August 1994.
24. Fritz Henglein, Christian Mossin. Polymorphic Binding-Time Analysis. In Proc. European Symposium on Programming (ESOP), Edinburgh, Scotland, Pages 287-301, April 1994.
25. Tatsurou Sekiguchi, Akinori Yonezawa. A Complete Type Inference System for Subtyped Recursive Types. In Proc.\ Int'l Symp.\ Theoretical Aspects of Computer Science (TACS), Sendai, Japan, Masami Hagiya, John C. Mitchell (eds.), Lecture Notes in Computer Science, Volume 789, Pages 667-686, April 1994.
26. Peter W. O'Hearn, Jon G. Riecke. Reducing Sequentiality and Block Structure to Parametric Polymorphism. In Proc. European Symp. on Programming (ESOP), Edinburgh, Scotland, April 1994.
27. Fritz Henglein, Jesper J\orgensen. Formally optimal boxing. In POPL '94: Proceedings of the 21st ACM SIGPLAN-SIGACT symposium on Principles of programming languages, Also DIKU Semantics Report D-179, Pages 213-226, New York, NY, USA, January 1994. download
28. Marcin Benke. Efficient type reconstruction in the presence of inheritance. In Proc. Mathematical Foundations of Computer Science (MFCS), A. M. Borzyszkowski, S. Sokolowski (eds.), Lecture Notes in Computer Science (LNCS), Vol. 711, Pages 272-280, 1993.
29. Alexander Aiken, Dexter Kozen, Moshe Vardi, Ed Wimmers. The Complexity of Set Constraints. In Proc. 1993 Conf. Computer Science Logic (CSL), September 1993.
30. Alexander Aiken, Edward L. Wimmers. Type Inclusion Constraints and Type Inference. In Proc. Conf. on Functional Programming Languages and Computer Architecture (FPCA), Copenhagen, Denmark, Pages 31-41, June 1993.
31. Guiseppe Longo. Types as Parameters. In Proc. Theory and Practice of Software Development (TAPSOFT), Orsay, France, M.-C. Gaudel, J.-P. Jouannaud (eds.), Lecture Notes in Computer Science, Volume 668, Pages 658-670, April 1993.
32. Geoffrey Smith. Polymorphic Type Inference with Overloading and Subtyping. In Proc. Theory and Practice of Software Development (TAPSOFT), Orsay, France, M.-C. Gaudel, J.-P. Jouannaud (eds.), Lecture Notes in Computer Science, Volume 668, Pages 671-685, April 1993.
33. Jerzy Tiuryn, Mitchell Wand. Type Reconstruction with Recursive Types and Atomic Subtyping. In Proc. Theory and Practice of Software Development (TAPSOFT), Orsay, France, M.-C. Gaudel, J.-P. Jouannaud (eds.), Lecture Notes in Computer Science, Volume 668, Pages 686-701, April 1993.
34. Pawel Urzyczyn. Type Reconstruction for $F_\omega$ is Undecidable. In Proc.\ Int'l Conf.\ on Typed Lambda Calculi and Applications (TLCA), Utrecht, The Netherlands, M. Bezem, J.F. Grotte (eds.), Lecture Notes in Computer Science, Volume 664, Pages 418-432, March 1993.
35. P.W. O'Hearn, R.D. Tennent. Relational Parametricity and Local Variables. In Proc. 20th Annual ACM SIGPLAN-SIGACT Symp. on Principles of Programming Languages, Pages 171-184, January 1993.
36. Martin Abadi, Luca Cardelli, Pierre-Louis Curien. Formal Parametric Polymorphism. In Proc. 20th Annual ACM SIGPLAN-SIGACT Symp. on Principles of Programming Languages, Pages 157-170, January 1993.
37. Robert Harper, Mark Lillibridge. Explicit Polymorphism and CPS Conversion. In Proc. 20th Annual ACM SIGPLAN-SIGACT Symp. on Principles of Programming Languages, Pages 206-219, January 1993.
38. Xavier Leroy. Polymorphism by Name for References and Continuations. In Proc. 20th Annual ACM SIGPLAN-SIGACT Symp. on Principles of Programming Languages, Pages 220-231, January 1993.
39. Mark P. Jones. A Theory of Qualified Types. In Proc. European Symposium on Programming (ESOP), Rennes, France, Lecture Notes in Computer Science, Vol. 582, 1992.
40. B. Monsuez. Polymorphic Typing by Abstract Interpretation. In Proc. 12th Conf. Foundations of Software Technology and Theoretical Computer Science (FST-TCS), New Delhi, India, Lecture Notes in Computer Science, December 1992.
41. Robert Harper, Mark Lillibridge. Polymorphic Type Assignment and CPS Conversion. In Proc. ACM SIGPLAN Workshop on Continuations (CW), San Francisco, California, Olivier Danvy, Carolyn Talcott (eds.), Stanford University Technical Report STAN-CS-92-1426, Pages 13-22, June 1992.
42. Stefan Kaes. Type Inference in the Presence of Overloading, Subtyping and Recursive Types. In Proc. ACM Conf. on LISP and Functional Programming (LFP), San Francisco, California, also in LISP Pointers, Vol. V, Number 1, January-March 1992, Pages 193-204, June 1992.
43. J. Tiuryn. Subtype Inequalities. In Proc. 7th Annual IEEE Symp. on Logic in Computer Science (LICS), Santa Cruz, California, Pages 308-315, June 1992.
44. Mark P. Jones. A Theory of Qualified Types. In Proc. 4th European Symposium on Programming (ESOP), Rennes, France, Bernd Krieg-Br\"uckner (ed.), Lecture Notes in Computer Science, Volume 582, Pages 287-306, February 1992.
45. A. Wright. Typing References by Effect Inference. In Proc. European Symposium on Programming (ESOP), Rennes, France, B. Krieg-Brückner (ed.), Lecture Notes in Computer Science, Vol. 582, Pages 473-491, February 1992.
46. P. O'Keefe, M. Wand. Type Inference for Partial Types is Decidable. In Proc. 4th European Symp. on Programming (ESOP), Rennes, France, B. Krieg-Brückner (ed.), Lecture Notes in Computer Science, Vol. 582, Pages 408-417, February 1992.
47. QingMing Ma. Parametricity as Subtyping. In Proc. 19th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programmin gLanguages (POPL), Albuquerque, New Mexico, Pages 281-292, January 1992.
48. A. Ohori. A Compilation Method for ML-Style Polymorphic Record Calculi. In Proc. 19th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programmin gLanguages (POPL), Albuquerque, New Mexico, Pages 154-165, January 1992.
49. B. Pierce. Bounded Quantification is Undecidable. In Proc. POPL '92, Pages 305-315, January 1992.
50. D. Remy. Typing Record Concatenation for Free. In Proc. 19th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programmin gLanguages (POPL), Albuquerque, New Mexico, Pages 166-176, January 1992.
51. K. Bruce, J. Mitchell. PER Models of Subtyping, Recursive Types and Higher-Order Polymorphism. In Proc. 19th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programmin gLanguages (POPL), Albuquerque, New Mexico, Pages 316-327, January 1992.
52. X. Leroy. Unboxed Objects and Polymorphic Typing. In Proc. 19th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programmin gLanguages (POPL), Alb uquerque, New Mexico, Pages 177-188, January 1992.
53. P. Lincoln, J. Mitchell. Algorithmic Aspects of Type Inference with Subtypes. In Proc. 19th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programmin Languages (POPL), Albuquerque, New Mexico, Pages 293-304, January 1992.
54. Nader H. Bshouty. Lower Bounds for Algebraic Computation Trees of Functions with Finite Domains. In ICCI, Pages 55-65, 1991.
55. L. Cardelli, S. Martini, J. Mitchell, A. Scedrov. An Extension of System F with Subtyping. In Proc. Int'l Conf. on Theoretical Aspects of Computer Software (TACS), Sendai, Japan, T. Ito, A. Meyer (eds.), Lecture Notes in Computer Science, Vol. 526, Pages 750-770, September 1991.
56. J. Mitchell. On Abstraction and the Expressive Power of Programming Languages. In Proc. Int'l Conf. on Theoretical Aspects of Computer Software (TACS), Sendai, Japan, T. Ito, A. Meyer (eds.), Lecture Notes in Computer Science, Vol. 526, Pages 290-310, September 1991.
57. G. Plotkin. A Semantics for Type Checking. In Proc. Int'l Conf. on Theoretical Aspects of Computer Software (TACS), Sendai, Japan, T. Ito, A. Meyer (eds.), Lecture Notes in Computer Science, Vol. 526, Pages 1-17, September 1991.
58. J. Reynolds. The Coherence of Languages with Intersection Types. In Proc. Int'l Conf. on Theoretical Aspects of Computer Science (TACS), Sendai, Japan, Lecture Notes in Computer Science, Vol. 526, September 1991.
59. S. Hirokawa. Principal Type-Schemes of BCI-Lambda-Terms. In Proc. Int'l Conf. on Theoretical Aspects of Computer Software (TACS), Sendai, Japan, T. Ito, A. Meyer (eds.), Lecture Notes in Computer Science, Vol. 526, Pages 631-650, September 1991.
60. H. Mairson. Outline of a Proof Theory of Parametricity. In Proc. Conf. on Functional Programming Languages and Computer Architecture (FPCA), Cambridge, Massachusetts, August 1991.
61. Fritz Henglein. Efficient Type Inference for Higher-Order Binding-Time Analysis. In Proc. Conf. on Functional Programming Languages and Computer Architecture (FPCA), Cambridge, Massachusetts, Pages 448-472, August 1991.
62. Fritz Henglein, Harry G. Mairson. The complexity of type inference for higher-order lambda calculi. In POPL '91: Proceedings of the 18th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, Pages 119-130, New York, NY, USA, January 1991. download
63. B. Duba, R. Harper, D. MacQueen. Typing First-Class Continuations in ML. In Proc. 18th Annual ACM Symposium on Principles of Programming Languages (POPL), Orlando, Florida, Pages 163-173, January 1991.
64. P. Jouvelot, D. Gifford. Algebraic Reconstruction of Types and Effects. In Proc. 18th Annual ACM Symposium on Principles of Programming Languages (POPL), Orlando, Florida, Pages 303-310, January 1991.
65. X. Leroy, P. Weis. Polymorphic Type Inference and Assignment. In Proc. 18th Annual ACM Symp. on Principles of Programming Languages, Orlando, Florida, Pages 291-302, January 1991.
66. J. Tiuryn. Type Inference Problems: A Survey. In Proc. Mathematical Foundations of Computer Science (MFCS), Lecture Notes in Computer Science, Pages 105-120, 1990.
67. S. Malecki. Generic Terms Having No Polymorphic Types. In Proc. 17th Int'l Coll. on Automata, Languages and Programming (ICALP), Lecture Notes in Computer Science, Vol. 443, July 1990.
68. A. Kfoury, J. Tiuryn. Type Reconstruction in Finite-Rank Fragments of the Polymorphic $\lambda$-Calculus. In Proc. 5th Annual IEEE Symp. on Logic in Computer Science (LICS), Philadelphia, Pennsylvania, Pages 2-11, June 1990.
69. A. Kfoury, J. Tiuryn, P. Urzyczyn. ML Typability is DEXPTIME-complete. In Proc. 15th Coll. on Trees in Algebra and Programming (CAAP), Copenhagen, Denmark, Lecture Notes in Computer Science, Vol. 431, Pages 206-220, May 1990.
70. A. Kfoury, J. Tiuryn, P. Urzyczyn. The Undecidability of the Semi-Unification Problem. In Proc. 22nd Annual ACM Symp. on Theory of Computation (STOC), Baltimore, Maryland, Pages 468-476, May 1990.
71. M. Hanus. A Functional and Logic Language with Polymorphic Types. In Proc. Int'l Symp. on Design and Implementation of Symbolic Computation Systems (DISCO), A. Miola (ed.), Lecture Notes in Computer Science, Vol. 429, Pages 215-224, April 1990.
72. H. Mairson. Deciding ML Typability is Complete for Deterministic Exponential Time. In Proc. 17th ACM Symp. on Principles of Programming Languages (POPL), January 1990.
73. M. Abadi, B. Pierce, G. Plotkin. Faithful Ideal Models for Recursive Polymorphic Types. In Proc. 1989 IEEE 4th Annual Symp. on Logic in Computer Science (LICS), Pages 216-225, 1989.
74. P. Canning, W. Cook, W. Hill, W. Olthoff, J. Mitchell. F-Bounded Polymorphism for Object-Oriented Programming. In Proc. Functional Programming Languages and Computer Architecture (FPCA), Pages 273-280, 1989.
75. M. Wand. Type Inference for Record Concatenation and Multiple Inheritance. In Proc. 1989 IEEE 4th Annual Symp. on Logic in Computer Science (LICS), Pages 92-97, 1989.
76. M. Wand, P. O'Keefe. On the Complexity of Type Inference with Coercion. In Proc. ACM Conf. on Functional Programming and Computer Architecture, 1989.
77. A. Ohori, P. Buneman. Static Type Inference for Parametric Classes. In Conf. Proc. Object-Oriented Programming: Systems, Languages, Applications (OOPSLA), appeared as SIGPLAN Notices, Vol. 24, No. 10, Pages 445-456, October 1989.
78. H. Lei\ss. Polymorphic Recursion and Semi-Unification (Extended Abstract). In Proc. 3rd Conf. Computer Science Logic, Karlsruhe, West Germany, October 1989.
79. A. Ohori. A Simple Semantics for ML Polymorphism. In Proc. Functional Programming Languages and Computer Architecture (FPCA), London, England, Pages 281-292, September 1989.
80. P. Wadler. Theorems for Free!. In Proc. Functional Programming Languages and Computer Architecture (FPCA), London, England, Pages 347-359, September 1989.
81. H. Boehm. Type Inference in the Presence of Type Abstraction. In Proc. SIGPLAN '89 Conf. on Programming Language Design and Implementation, Pages 192-206, June 1989.
82. A. Kfoury, J. Tiuryn, P. Urzyczyn. Computational Consequences and Partial Solutions of a Generalized Unification Problem. In Proc. 4th IEEE Symposium on Logic in Computer Science (LICS), June 1989.
83. H. Lei\ss. A Semi-Unification Algorithm? - Extended Abstract. In Proc. UNIF '89, Burkert, Nutt (eds.), Lambrecht, Germany, June 1989.
84. D. Leivant. Finitely Stratified Polymorphism. In Proc. Logic in Computer Science, June 1989.
85. J. O'Toole Jr, D. Gifford. Type Reconstruction with First-Class Polymorphic Values. In Proc. SIGPLAN '89 Conf. on Programming Language Design and Implementation, Pages 207-217, June 1989.
86. M. Hanus. Horn Clause Programs with Polymorphic Types: Semantics and Resolution. In Proc. Int'l J't Conf. on Theory and Practice of Software Development (Vol. 2), Lecture Notes in Computer Science, Vo.l. 352, Pages 225-240, Barcelona, Spain, March 1989.
87. P. Kanellakis, J. Mitchell. Polymorphic Unification and ML Typing (Extended Abstract). In Proc. 16th Annual ACM Symp. on Principles of Programming Languages, to appear, January 1989.
88. G. Monteleone. Generalized Conjunctive Types. In Proc. 16th Annual ACM Symp. on Principles of Programming Languages, Pages 242-249, January 1989.
89. P. Wadler, S. Blott. How to Make ad-hoc Polymorphism Less ad hoc. In Proc. 16th Annual ACM Symp. on Principles of Programming Languages, Pages 60-76, January 1989.
90. Didier Rémy. Typechecking Records and Variants in a Natural Extension of ML. In Proc. 16th Annual ACM Symp. on Principles of Programming Languages, Pages 77-88, January 1989.
91. R. Dietrich, F. Hagl. A Polymorphic Type System with Subtypes for Prolog. In Proc. European Symposium on Programming (ESOP), Lecture Notes in Computer Science 300, Pages 79-93, 1988.
92. Y. Fuh, P. Mishra. Type Inference with Subtypes. In Proc. 2nd European Symp. on Programming, Lecture Notes in Computer Science 300, Pages 94-114, 1988.
93. A. Scedrov. A Guide to Polymorphic Types. In Logic and Computer Science, Lecture Notes in Mathematics, Vol. 1429, Pages 111-150, 1988.
94. S. Thatte. Type Inference with Partial Types. In Proc. Int'l Coll. on Automata, Languages and Programming (ICALP), Lecture Notes in Computer Science, Pages 615-629, 1988.
95. U. Reddy. Notions of Polymorphism for Predicate Logic Programs. In Proc. Int'l Conf. on Logic Programming, Pages 17-34, Seattle, Washington, August 1988.
96. M. van Emden. Conditional Answers for Polymorphic Type Inference. In Proc. Int'l Conf. on Logic Programming, Pages 590-603, Seattle, Washington, August 1988.
97. P. Voda. Types of Trilogy. In Proc. Int'l Conf. on Logic Programming, Pages 580-589, Seattle, Washington, August 1988.
98. J. Xu, D. Warren. A Type Inference System for Prolog. In Proc. Int'l Conf. on Logic Programming, Pages 604-619, Seattle, Washington, August 1988.
99. Fritz Henglein. Type inference and semi-unification. In LFP '88: Proceedings of the 1988 ACM conference on LISP and functional programming, Pages 184-197, New York, NY, USA, July 1988. download
100. A. Ohori, P. Buneman. Type Inference in a Database Programming Language. In Proc. 1988 ACM Conf. on LISP and Functional Programming, Pages 174-183, July 1988.
101. F. Pfenning. Partial Polymorphic Type Inference and Higher-Order Unification. In Proc. 1988 ACM LISP and Functional Programming Conf, Pages 153-163, July 1988.
102. A. Kfoury, J. Tiuryn, P. Urzyczyn. On the Computational Power of Universally Polymorphic Recursion. In Proc. Symp. on Logic in Computer Science, Pages 72-81, June 1988.
103. H. Azzoune. Type Inference in Prolog. In Proc. 9th Int'l Conf. on Automated Deduction, Lecture Notes in Computer Science 310, Pages 258-277, Argonne, Illinois, May 1988.
104. J. Lucassen, D. Gifford. Polymorphic Effect Systems. In Proc. 15th ACM Symp. on Principles of Programming Languages, Pages 47-57, San Diego, California, January 1988.
105. R. Stansifer. Type Inference with Subtypes. In Proc. 15th ACM Symp. on Principles of Programming Languages, Pages 88-97, San Diego, California, January 1988.
106. L. Cardelli. Structural Subtyping and the Notion of Power Type. In Title of book Proc. 15th Annual ACM Symp. on Principles of Programming Languages, Pages 70-79, January 1988.
107. A. Kfoury, J. Tiuryn, P. Urzyczyn. A Proper Extension of ML with an Effective Type-Assignment. In Proc. 15th Annual ACM Symp. on Principles of Programming Languages, Pages 58-69, January 1988.
108. V. Breazu-Tannen, A. Meyer. Polymorphism is Conservative over Simple Types. In Proc. Symp. on Logic in Comp. Sci. '87, Pages 7-17, 1987.
109. N. Mendler. Recursive Types and Type Constraints in Second-Order Lambda Calculus. In Proc. Symp. on Logic in Computer Science (LICS), Pages 30-36, 1987.
110. J. Zobel. Derivation of Polymorphic Types for PROLOG Programs. In Proc. 4th Int'l. Conf. on Logic Programming, Vol. 2, Pages 817-838, Melbourne, Australia, 1987.
111. J. Young, P. O'Keefe. Experience with a Type Evaluator. In Proc. Workshop on Partial Evaluation and Mixed Computation, Denmark, D. Bjorner, A. Ershov, N. Jones (eds.), Pages 573-582, October 1987.
112. H. Lei\ss. On Type Inference for Object-Oriented Programming Languages. In Proc. 1st Workshop on Computer Science Logic, October 1987.
113. K. Horiuchi, T. Kanamori. Polymorphic Type Inference in Prolog by Abstract Interpretation. In Proc. Logic Programming, Lecture Notes in Computer Science, Vol. 315, Pages 195-214, Tokyo, Japan, June 1987.
114. M. Wand. Complete Type Inference for Simple Objects. In Proc. Symp. on Logic in Comp. Sci, Pages 37-44, June 1987.
115. V. Breazu-Tannen, T. Coquand. Extensional Models for Polymorphism. In Proc. Int'l Joint Conf. on Theory and Practice of Software Development (TAPSOFT), Lecture Notes in Computer Science 250, Pages 291-307, Pisa, Italy, March 1987.
116. A. Meyer, J. Mitchell, E. Moggi, R. Statman. Empty Types in Polymorphic Lambda Calculus. In Proc. 14th Annual ACM Symp. on Principles of Programming Languages, Pages 253-262, January 1987.
117. L. Cardelli. Typechecking Dependent Types and Subtypes. In Proc. Foundations of Logic and Functional Programming, Lecture Notes in Computer Science, Vol. 306, Pages 45-57, December 1986.
118. J. Mitchell. A Type-Inference Approach to Reduction Properties and Semantics of Polymorphic Expressions (Summary). In Proc. ACM Conference on LISP and Functional Programming, Pages 308-319, August 1986.
119. J. Mitchell. Representation Independence and Data Abstraction. In Proc. 13th ACM Symp. on Principles of Programming Languages, Pages 263-276, St. Petersburg Beach, Florida, January 1986.
120. H. Boehm. Partial Polymorphic Type Inference is Undecidable. In Proc. 26th Annual Symp. on Foundations of Computer Science, Pages 339-345, October 1985.
121. R. Nikhil. Practical Polymorphism. In Proc. Functional Programming Languages and Computer Architecture, Pages 319-333, Nancy, France, September 1985.
122. J. Mitchell, G. Plotkin. Abstract Types have Existential Type. In Proc. 12th ACM Symp. on Principles of Programming Languages, Pages 37-51, January 1985.
123. P. Mishra, U. Reddy. Declaration-Free Type Checking. In Proc. 12th ACM Symp. on Principles of Programming Languages, Pages 7-21, January 1985.
124. M. Wand. Embedding Type Structure in Semantics. In Proc. 12th ACM Symp. on Principles of Programming Languages, Pages 1-6, New Orleans, Louisiana, January 1985.
125. R. Cartwright. Types as Intervals. In Proc. 12th ACM Symp. on Principles of Programming Languages, Pages 22-36, New Orleans, Louisiana, January 1985.
126. J. Mitchell. Coercion and Type Inference. In Proc. 11th ACM Symp. on Principles of Programming Languages (POPL), 1984.
127. P. Mishra. Towards a Theory of Types in Prolog. In Proc. 1984 IEEE Symp. on Logic Programming, 1984.
128. A. Mycroft. Polymorphic Type Schemes and Recursive Definitions. In Proc. 6th Int. Conf. on Programming, LNCS 167, 1984.
129. T. Katayama. Type Inference and Type Checking for Functional Programming Languages - A Reduced Computation Approach. In Conf. Rec. of the 1984 ACM Symp. on LISP and Functioal Programming, Pages 263-272, August 1984.
130. N. McCracken. The Typechecking of Programs with Implicit Type Structure. In Proc. Int'l Symp. on Semantics of Data Types, Lecture Notes in Computer Science, Vol. 173, Pages 301-316, June 1984.
131. J. Mitchell. Type Inference and Type Containment. In Proc. Int'l Symp. on Semantics of Data Types, LNCS 173, Pages 257-277, June 1984.
132. M. Wand. A Types-as-Sets Semantics for Milner-Style Polymorphism. In Proc. 11th ACM Symp. on POPL, Pages 158-164, January 1984.
133. Michael Ben-Or. Lower Bounds for Algebraic Computation Trees (Preliminary Report). In STOC, Pages 80-86, 1983.
134. D. Leivant. Structural semantics for polymorphic data types. In Proc. 1983 POPL, 1983.
135. L. Meertens. Incremental Polymorphic Type Checking in B. In Proc. 10th ACM Symp. on Principles of Programming Languages (POPL), Pages 265-275, 1983.
136. D. MacQueen, R. Sethi. A Semantic Model of Types for Applicative Languages. In Proc. SIGPLAN/SIGACT/SIGART Symp. on LISP and Functional Programming, Pages 243-252, Pittsburgh, Pennsylvania, 1982.
137. L. Damas, R. Milner. Principal Type Schemes for Functional Programs. In Proc. 9th Annual ACM Symp. on Principles of Programming Languages, Pages 207-212, January 1982.
138. Nicholas Pippenger. Comparative Schematology and Pebbling with Auxiliary Pushdowns (Preliminary Version). In STOC, Pages 351-356, 1980.
139. A. Borodin, S. Cook. A Time-Space Tradeoff for Sorting on a General Sequential Model of Computation. In Proc. 1980 STOC, Pages 294-301, 1980.
140. J. Reynolds. Using Category Theory to Design Conversions and Generic Operators. In Proc. Semantics-Directed Compiler Generation, Lecture Notes in Computer Science, Vol. 94, Pages 211-258, 1980.
141. QingMing Ma, John C. Reynolds. Types, Abstraction, and Parametric Polymorphism, Part 2. In Proc. xxx, 0.
142. Adolfo Piperno, Simona Ronchi della Rocca. Type Inference and Extensionality. In Proc. LICS '94 (?), Pages 196-205, 0.

Technical Reports

1. Sian Jha, Jens Palsberg, Tian Zhao, Fritz Henglein. Efficient Type Matching. TOPPS Report D-474 Department of Computer Science, University of Copenhagen (DIKU), 2002.
2. Martin Emms, Hans Lei\ss. Extending the Type Checker for SML by Polymorphic Recursion - A Correctness Proof. Research Report Centrum f\"ur Informations- und Sprachverarbeitung, Universit\"at M\"unchen, No 96, 1996.
3. Jakob Rehof. Minimal Typings in Atomic Subtyping (Summary). Research Report DIKU, University of Copenhagen, 1996.
4. Chris Stone, Robert Harper. A Type-Theoretic Account of Standard ML 1996 (Version 1). Research Report School of Computer Science, Carnegie Mellon University, No 0, 1996.
5. Jerzy Tiuryn. A Sequent Calculus for Subtyping Polymorphic Types. Research Report Institute of Informatics, Warsaw University, No 96, April 1996.
6. Martin Emms. Documentation for polyrec_sml: An extension of SML with typechecking for polymorphic recursion. Research Report Centrum f\"ur Informations- und Sprachverarbeitung, Universit\"at M\"unchen, No 95, 1995.
7. Jerzy Tiuryn, Pawel Urzyczyn. The Subtyping Problem for Second-Order Types is Undecidable. Research Report Institute of Informatics, Warsaw University, No 95, December 1995.
8. Jens Palsberg, Mitchell Wand, Patrick O'Keefe. Type Inference with Non-structural Subtyping. Research Report BRICS, Dept. of Computer Science, Aarhus University, No 0, April 1995.
9. J.B. Wells. Typability and Type Checking in the Second-Order $\lambda$-Calculus Are Equivalent and Undecidable. Research Report Boston University, Computer Science Department, No 93, January 1994.
10. A.J. Kfoury, J.B. Wells. A Direct Algorithm for Type Inference in the Rank 2 Fragment of the Second-Order $\lambda$-Calculus. Research Report Boston University, No 93, November 1993.
11. John Greiner. Standard ML Weak Polymorphism Can Be Sound. Research Report Carnegie Mellon University, School of Computer Science, No 0, September 1993.
12. Alexander Aiken, Dexter Kozen, Ed Wimmers. Decidability of Systems of Set Constraints with Negative Constraints. Research Report Cornell University, No 93, June 1993.
13. Andrew Wright. Polymorphism for Imperative Languages without Imperative Types. Research Report Rice University, No 0, February 1993.
14. Xavier Leroy. Polymorphic Typing of an Algorithmic Language. Rapports de Recherche INRIA, No 1778, October 1992.
15. Laurence Puel, Asc\'ander Su\'arez. Extended Polymorphic Type Checking in ML. Research Report Université Paris Sud, No 762, June 1992.
16. J.-P. Talpin, P. Jouvelot. The Type and Effect Discipline (Extended Version). Research Report Ecole des Mines de Paris, No 0, December 1991.
17. B. Pierce. Bounded Quantification is Undecidable. Research Report Carnegie Mellon University, No 0, July 1991.
18. J. Talpin, P. Jouvelot. The Type and Effect Discipline. Research Report Ecole des Mines de Paris, No 0, July 1991.
19. A. Wright, M. Felleisen. A Syntactic Approach to Type Soundness. Research Report Rice University, No 91, April 1991.
20. J. Talpin, P. Jouvelot. Polymorphic Type Region and Effect Inference. Research Report Ecole des Mines de Paris, No 0, February 1991.
21. J. Talpin, P. Jouvelot. Polymorphic Type, Region and Effect Inference. Research Report Ecole des Mines de Paris, No 0, February 1991.
22. D. Shin. Toward Optimal Type Checking for the Polymorphic Type System of Prolog. Research Report Int'l Inst. for Advanced Study of Social Information Science, Fujitsu Lab's, Ltd, No 0, December 1990.
23. Fritz Henglein. A Lower Bound for Full Polymorphic Type Inference: Girard-Reynolds Typability is DEXPTIME-hard. RUU-CS-90-14 Utrecht University, April 1990.
24. P. Curtis. Constrained Quantification in Polymorhic Type Analysis. Research Report Xerox Parc, No 0, February 1990.
25. H. Lei\ss. Semi-Unification and Type Inference for Polymorphic Recursion. Research Report Siemens, No 0, 1989.
26. A. Kfoury, J. Tiuryn. Type Reconstruction in Finite Rank Fragments of the Second-Order Lambda Calculus. Research Report Boston University, No 0, October 1989.
27. A. Kfoury, J. Tiuryn, P. Urzyczyn. The Undecidability of the Semi-Unification Problem. Research Report Boston University, No 0, October 1989.
28. A. Kfoury, J. Tiuryn, P. Urzyczyn. An Analysis of ML Typability. Research Report Boston University, No 0, October 1989.
29. Peter de Bruin. Naturalness of Polymorphism. Research Report U. of Groningen, No 8916, September 1989.
30. Fritz Henglein. Simple Type Inference and Unification. SETL Newsletter Courant Institute of Mathematical Sciences, New York University, No 232, October 1988.
31. K. Walker. A Type Inference System for Icon. Research Report University of Arizona, No 88, July 1988.
32. Catherine Dubois, Fritz Henglein. A First-Order Axiomatization of Parametric Polymorphism and Dynamic Overloading and its Typol Specification. SETL Newsletter New York University, No 224, May 1988.
33. K. Bruce, G. Longo. A Modest Model of Records, Inheritance and Bounded Quantification. Research Report CMU, No 0, April 1988.
34. T. Coquand, Gunter C, Winskel G.. Domain Theoretic Models of Polymorphism. Research Report University of Cambridge, No 116, September 1987.
35. G. Cormack, M. Judd, A. Wright. Polymorphism in a Compiled Language. Research Report University of Waterloo, No 0, 1986.
36. R. Cartwright. Types as Intervals. Research Report Rice University, No 84, 1984.

Miscellaneous

1. Peter O'Hearn, John C. Reynolds. From Algol to Polymorphic Linear Lambda-Calculus. Manuscript, April 1997.
2. Jakob Rehof. Introduction to Subtyping. 1996.
3. Nikolaj Bj\orner. Minimal Typing Derivations. DIKU Student Report, July 1992.
4. M. Odersky. Locally Polymorphic Types. submitted to SIGPLAN '91, November 1990.
5. J. Reynolds. Even Normal Forms can be Hard to Type. Extended abstract, December 1989.
6. A. Borodin, F. Fich, F. Meyer auf der Heide, E. Upfal, A. Wigderson. A Time-Space Tradeoff for Element Distinctness. Manuscript, 1983.
7. J. Gallier. On Girard's Candidats de Reductibilite - Some Polymorphic Thoughts. 0.
8. J. Mitchell. Relating Type Theories. 0.
9. J. Reynolds. A Short History of Set-Theoretic Models of the Polymorphic Typed Lambda Calculus. 0.
10. A. Scedrov. Semantic Studies of Polymorphism. 0.

Dissertations

1. Jesper J\orgensen. A Calculus for Boxing Analysis of Polymorphically Typed Languages. PhD Thesis DIKU, University of Copenhagen, October 1995.
2. Jean-Pierre Talpin. Aspects Théoriques et Pratiques de l'Inférence de Type et d'Effets. PhD Thesis l'Ecole Nationale Supérieure des Mines de Paris, May 1993.
3. Xavier Leroy. Typage polymorphe d'un langage algorithmique. PhD Thesis University Paris VII, June 1992.
4. B. Pierce. Programming with Intersection Types and Bounded Polymorphism. PhD Thesis School of Computer Science, Carnegie Mellon University, December 1991.
5. Geoffrey Seward Smith. Polymorphic Type Inference for Languages with Overloading and Subtyping. PhD Thesis Cornell University, August 1991.
6. G. Smolka. Logic Programming Over Polymorphically Order-Sorted Types. PhD Thesis Universitaet Kaiserslautern, May 1989.
7. Fritz Henglein. Polymorphic Type Inference and Semi-Unification. PhD Thesis Rutgers University, April 1989.
8. J.M. Lucassen. Types and Effects towards the Integration of Functional and Imperative Programming. PhD Thesis Massachusetts Institute of Technology (MIT), August 1987.
9. L. Damas. Type Assignment in Programming Languages. PhD Thesis University of Edinburgh, 1984.
10. C. Ben-Yelles. Type-assignment in the Lambda-calculus. PhD Thesis University College, Swansea, 1979.
11. Ch. Ben-Yelles. Type Assignment in the Lambda-Calculus: Syntax and Semantics. PhD Thesis Department of Pure Mathematics, University College of Swansea, September 1979.

Master's thesis

1. Jakob Rehof. Polymorphic Dynamic Typing - Aspects of Proof Theory and Inference. Master's theses DIKU, University of Copenhagen, March 1995.

This material is presented to ensure timely dissemination of scholarly and technical work. Copyright and all rights therein are retained by authors or by other copyright holders. All persons copying this information are expected to adhere to the terms and constraints invoked by each author's copyright. These works may not be reposted without the explicit permission of the copyright holder.