References

---

References

Abadi, Mart n. Secrecy by typing in security protocols. Journal of the ACM, 46(5): 749–786, September 1999. Summary in Theoretical Aspects of Computer Software (TACS), Sendai, Japan, 1997; volume 1281 of Springer LNCS.

Abadi, Mart n, Anindya Banerjee, Nevin Heintze, and Jon G. Riecke. A core calculus of dependency. In ACM Symposium on Principles of Programming Languages (POPL), San Antonio, Texas, pages 147–160, 1999.

Abadi, Mart n and Luca Cardelli. On subtyping and matching. In European Conference on Object-Oriented Programming (ECOOP), pages 145–167, 1995.

Abadi, Mart n and Luca Cardelli. A Theory of Objects. Springer-Verlag, 1996.

Abadi, Mart n, Luca Cardelli, and Pierre-Louis Curien. Formal parametric polymorphism. Theoretical Computer Science, 121(1–2):9–58, 6 December 1993. Summary in ACM Symposium on Principles of Programming Languages (POPL), Charleston, South Carolina, 1993.

Abadi, Mart n, Luca Cardelli, Pierre-Louis Curien, and Jean-Jacques L vy. Explicit substitutions. Journal of Functional Programming, 1(4):375–416, 1991a. Summary in ACM Symposium on Principles of Programming Languages (POPL), San Francisco, California, 1990.

Abadi, Mart n, Luca Cardelli, Benjamin Pierce, and Gordon Plotkin. Dynamic typing in a statically typed language. ACM Transactions on Programming Languages and Systems, 13(2):237–268, April 1991b. Summary in ACM Symposium on Principles of Programming Languages (POPL), April 1989.

Abadi, Mart n, Luca Cardelli, Benjamin Pierce, and Didier R my. Dynamic typing in polymorphic languages. Journal of Functional Programming, 5(1):111–130, January 1995. Summary in ACM SIGPLAN Workshop on ML and its Applications, June 1992.

Abadi, Mart n, Luca Cardelli, and Ramesh Viswanathan. An interpretation of objects and object types. In ACM Symposium on Principles of Programming Languages (POPL), St. Petersburg Beach, Florida, pages 396–409, 1996.

Abadi, Mart n and Marcelo P. Fiore. Syntactic considerations on recursive types. In Proceedings of the 11th Annual IEEE Symposium on Logic in Computer Science, LICS '96, pages 242–252. IEEE Computer Society Press, Los Alamitos, CA, July 1996.

Abelson, Harold and Gerald Sussman. Structure and Interpretation of Computer Programs. MIT Press, New York, 1985. Second edition, 1996.

Abramsky, Samson, Radha Jagadeesan, and Pasquale Malacaria. Full abstraction for pcf. Information and Computation, 163(2):409–470, December 2000.

Aczel, Peter. An introduction to inductive definitions. In Jon Barwise, editor, Hand-book of Mathematical Logic, number 90 in Studies in Logic and the Foundations of Mathematics, pages 739–782. North Holland, 1977.

Aczel, Peter. Non-Well-Founded Sets. Stanford Center for the Study of Language and Information,1988. CSLI Lecture Notes number 14.

Agesen, Ole, Stephen N. Freund, and John C. Mitchell. Adding type parameterization to the Java language. In ACM Symposium on Object Oriented Programming: Systems, Languages, and Applications (OOPSLA), pages 49–65, Atlanta, GA, October 1997.

Aho, Alfred V., Ravi Sethi, and Jeffrey D. Ullman. Compilers: Principles, Techniques, and Tools. Addison-Wesley, Reading, MA, USA, 1986.

Aiken, Alexander and Edward L. Wimmers. Type inclusion constraints and type inference. In ACM Symposium on Functional Programming Languages and Computer Architecture (FPCA), pages 31–41, 1993.

Amadio, Roberto M. and Luca Cardelli. Subtyping recursive types. ACM Transactions on Programming Languages and Systems, 15(4):575–631, 1993. Summary in ACM Symposium on Principles of Programming Languages (POPL), Orlando, Florida, pp. 104–118; also DEC/Compaq Systems Research Center Research Report number 62, August 1990.

Appel, Andrew W. Modern Compiler Implementation in ML. Cambridge University Press, 1998.

Appel, Andrew W. and Marcelo J. R. Gon alves. Hash-consing garbage collection. Technical Report CS-TR-412-93, Princeton University, Computer Science Department,1993.

Arbib, Michael and Ernest Manes. Arrows, Structures, and Functors: The Categorical Imperative. Academic Press, 1975.

Ariola, Zena M., Matthias Felleisen, John Maraist, Martin Odersky, and Philip Wadler. A call-by-need lambda calculus. In ACM Symposium on Principles of Programming Languages (POPL), San Francisco, California, pages 233–246, January 1995.

Arnold, Ken and James Gosling. The Java Programming Language. Addison Wesley, 1996.

Arnold, Ken, Ann Wollrath, Bryan O'Sullivan, Robert Scheifler, and Jim Waldo. The Jini specification. Addison-Wesley, Reading, MA, USA, 1999.

Asperti, Andrea and Giuseppe Longo. Categories, Types, and Structures: An Introduction to Category Theory for the Working Computer Scientist. MIT Press, 1991.

Aspinall, David. Subtyping with singleton types. In Computer Science Logic (CSL), Kazimierz,Poland, pages 1–15. Springer-Verlag, 1994.

Aspinall, David and Adriana Compagnoni. Subtyping dependent types. Information and Computation, 266(1–2):273–309, September 2001. Preliminary version in IEEE Symposium on Logic in Computer Science (LICS), 1996.

Astesiano, Egidio. Inductive and operational semantics. In E. J. Neuhold and M. Paul, editors, Formal Description of Programming Concepts, IFIP State-of-the-Art Reports, pages 51–136. Springer-Verlag, 1991.

Augustsson, Lennart. A compiler for Lazy ML. In ACM Symposium on Lisp and Functional Programming (LFP), Austin, Texas, pages 218–227, August 1984.

Augustsson, Lennart. Cayenne — a language with dependent types. In International Conference on Functional Programming (ICFP), Baltimore, Maryland, USA, pages 239–250, 1998.

Baader, Franz and Tobias Nipkow. Term Rewriting and All That. Cambridge University Press, 1998.

Baader, Franz and J rg Siekmann. Unification theory. In D. M. Gabbay, C. J. Hogger, and J. A. Robinson, editors, Handbook of Logic in Artificial Intelligence and Logic Programming, volume 2, Deduction Methodologies, pages 41–125. Oxford University Press, Oxford, UK, 1994.

Backus, John. Can programming be liberated from the von Neumann style? A functional style and its algebra of programs. Communications of the ACM, 21(8):613– 641, August 1978. Reproduced in Selected Reprints on Dataflow and Reduction Architectures, ed. S. S. Thakkar, IEEE, 1987, pp. 215–243, and in ACM Turing Award Lectures: The First Twenty Years, ACM Press, 1987, pp. 63–130.

Backus, John. The history of Fortran I, II, and III. In Wexelblat, editor,History of Programming Languages, pages 25–45. Academic Press, 1981.

Bainbridge, E. Stewart, Peter J. Freyd, Andre Scedrov, and Philip J. Scott. Functorial polymorphism. Theoretical Computer Science, 70(1):35–64, 1990. Corrigendum in TCS 71(3), 431.

Baldan, Paolo, Giorgio Ghelli, and Alessandra Raffaet . Basic theory of F-bounded quantification. Information and Computation, 153(1):173–237, 1999.

Barendregt, Henk P. The Lambda Calculus. North Holland, revised edition, 1984.

Barendregt, Henk P. Functional programming and lambda calculus. In Jan van Leeuwen, editor, Handbook of Theoretical Computer Science, Volume B, chapter 7, pages 321–364. Elsevier / MIT Press, 1990.

Barendregt, Henk P. Introduction to generalized type systems. Journal of Functional Programming, 1(2):125–154, 1991.

Barendregt, Henk P. Lambda calculi with types. In Abramsky, Gabbay, and Maibaum, editors,Handbook of Logic in Computer Science, volume II. Oxford University Press, 1992.

Barras, Bruno, Samuel Boutin, Cristina Cornes, Judicael Courant, Jean-Christophe Filliatre, Eduardo Gimenez, Hugo Herbelin, Gerard Huet, Cesar Munoz, Chetan Murthy, Catherine Parent, Christine Paulin-Mohring, Amokrane Saibi, and Benjamin Werner. The Coq proof assistant reference manual : Version 6.1. Technical Report RT-0203, Inria (Institut National de Recherche en Informatique et en Automatique), France, 1997.

Barwise, Jon and Lawrence Moss. Vicious Circles: On the Mathematics of Non-wellfounded Phenomena. Cambridge University Press, 1996.

Berardi, Stefano. Towards a mathematical analysis of the Coquand-Huet calculus of constructions and the other systems in Barendregt's cube. Technical report, Department of Computer Science, CMU, and Dipartimento Matematica, Universita di Torino, 1988.

Berger, Ulrich. Program extraction from normalization proofs. In Marc Bezem and Jan Friso Groote, editors, Typed Lambda Calculi and Applications, number 664 in Lecture Notes in Computer Science,pages 91–106, Utrecht, The Netherlands, March 1993. Springer-Verlag

Berger, Ulrich and Helmut Schwichtenberg. An inverse of the evaluation functional for typed λ-calculus. In Gilles Kahn, editor, IEEE Symposium on Logic in Computer Science (LICS), pages 203–211, Amsterdam, The Netherlands, July 1991. IEEE Computer Society Press.

Birtwistle, Graham M., Ole-Johan Dahl, Bjorn Myhrhaug, and Kristen Nygaard. Simula Begin. Studentlitteratur (Lund, Sweden), Bratt Institut fuer neues Lernen (Goch, FRG), Chartwell-Bratt Ltd (kent, England), 1979.

Bobrow, Daniel G., Linda G. DeMichiel, Richard P. Gabriel, Sonya E. Keene, Gregor Kiczales, and David A. Moon. Common Lisp Object System specification X3J13 document 88-002R. SIGPLAN Notices, 23, 1988.

Boehm, Hans-J. Partial polymorphic type inference is undecidable. In 26th Annual Symposium on Foundations of Computer Science, pages 339–345. IEEE, October 1985.

Boehm, Hans-J. Type inference in the presence of type abstraction. In ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), Portland,Oregon, pages 192–206, June 1989.

B hm, Corrado and Alessandro Berarducci. Automatic synthesis of typed Λ-programs on term algebras. Theoretical Computer Science, 39(2–3):135–154, August 1985.

Bono, Viviana and Kathleen Fisher. An imperative first-order calculus with object extension. In European Conference on Object-Oriented Programming (ECOOP), 1998.

Bono, Viviana, Amit J. Patel, and Vitaly Shmatikov. A core calculus of classes and mixins. In European Conference on Object-Oriented Programming (ECOOP), volume 1628 of Lecture Notes in Computer Science, pages 43–66. Springer-Verlag, June 1999a.

Bono, Viviana, Amit J. Patel, Vitaly Shmatikov, and John C. Mitchell. A core calculus of classes and objects. In Fifteenth Conference on the Mathematical Foundations of Programming Semantics, April 1999b.

Bracha, Gilad, Martin Odersky, David Stoutamire, and Philip Wadler. Making the future safe for the past: Adding genericity to the Java programming language. In Craig Chambers, editor, ACM Symposium on Object Oriented Programming: Systems, Languages, and Applications (OOPSLA), ACM SIGPLAN Notices volume 33 number 10, pages 183–200, Vancouver, BC, October 1998.

Braithwaite, Richard B. The Foundations of Mathematics: Collected Papers of Frank P. Ramsey. Routledge and Kegan Paul, London, 1931.

Brandt, Michael and Fritz Henglein. Coinductive axiomatization of recursive type equality and subtyping. In Roger Hindley, editor, Proc. 3d Int'l Conf. on Typed Lambda Calculi and Applications (TLCA), Nancy, France, April 2–4, 1997, volume 1210 of Lecture Notes in Computer Science (LNCS), pages 63–81. Springer-Verlag, April 1997. Full version in Fundamenta Informaticae, Vol. 33, pp. 309–338, 1998.

Breazu-Tannen, Val, Thierry Coquand, Carl Gunter, and Andre Scedrov. Inheritance as implicit coercion. Information and Computation, 93:172–221, 1991. Also in Carl A. Gunter and John C. Mitchell, editors, Theoretical Aspects of Object-Oriented Programming: Types, Semantics, and Language Design (MIT Press, 1994).

Bruce, Kim B. The equivalence of two semantic definitions for inheritance in object-oriented languages. In Proceedings of Mathematical Foundations of Programming Semantics, Pittsburgh, PA, March 1991.

Bruce, Kim B. A paradigmatic object-oriented programming language: Design, static typing and semantics. Journal of Functional Programming, 4(2), April 1994. Summary in ACM Symposium on Principles of Programming Languages (POPL), Charleston, South Carolina, under the title "Safe type checking in a statically typed object-oriented programming language".

Bruce, Kim B. Foundations of Object-Oriented Languages: Types and Semantics. MIT Press, 2002.

Bruce, Kim B., Luca Cardelli, Giuseppe Castagna, the Hopkins Objects Group (Jonathan Eifrig, Scott Smith, Valery Trifonov), Gary T. Leavens, and Benjamin Pierce. On binary methods. Theory and Practice of Object Systems, 1(3):221–242, 1996.

Bruce, Kim B., Luca Cardelli, and Benjamin C. Pierce. Comparing object encodings. Information and Computation, 155(1/2):108–133, November 1999. Special issue of papers from Theoretical Aspects of Computer Software (TACS 1997). An earlier version appeared as an invited lecture in the Third International Workshop on Foundations of Object Oriented Languages (FOOL 3), July 1996.

Bruce, Kim B. and Giuseppe Longo. A modest model of records, inheritance, and bounded quantification. Information and Computation, 87:196–240, 1990. Also in Carl A. Gunter and John C. Mitchell, editors, Theoretical Aspects of Object-Oriented Programming: Types, Semantics, and Language Design (MIT Press, 1994). An earlier version appeared in the proceedings of the IEEE Symposium on Logic in Computer Science, 1988.

Bruce, Kim B. and John Mitchell. PER models of subtyping, recursive types and higher-order polymorphism. In ACM Symposium on Principles of Programming Languages (POPL), Albuquerque, New Mexico, January 1992.

Bruce, Kim B., Leaf Petersen, and Adrian Fiech. Subtyping is not a good "match" for object-oriented languages. In European Conference on Object-Oriented Programming (ECOOP), volume 1241 of Lecture Notes in Computer Science, pages 104–127. Springer-Verlag, 1997.

Buneman, Peter and Benjamin Pierce. Union types for semistructured data. In Internet Programming Languages. Springer-Verlag, September 1998. Proceedings of the International Database Programming Languages Workshop. LNCS 1686.

Burstall, Rod and Butler Lampson. A kernel language for abstract data types and modules. In G. Kahn, D. MacQueen, and G. Plotkin, editors, Semantics of Data Types, volume 173 of Lecture Notes in Computer Science, pages 1–50. Springer-Verlag, 1984.

Burstall, Rod M. Proving properties of programs by structural induction. The Computer Journal, 12(1):41–48, 1969.

Canning, Peter, William Cook, Walt Hill, and Walter Olthoff. Interfaces for strongly-typed object-oriented programming. In ACM Symposium on Object Oriented Programming: Systems, Languages, and Applications (OOPSLA), pages 457–467, 1989a.

Canning, Peter, William Cook, Walter Hill, Walter Olthoff, and John Mitchell. F-bounded quantification for object-oriented programming. In ACM Symposium on Functional Programming Languages and Computer Architecture (FPCA), pages 273–280, September 1989b.

Canning, Peter, Walt Hill, and Walter Olthoff. A kernel language for object-oriented programming. Technical Report STL-88-21, Hewlett-Packard Labs, 1988.

Cardelli, Luca. A semantics of multiple inheritance. In G. Kahn, D. MacQueen, and G. Plotkin, editors, Semantics of Data Types, volume 173 of Lecture Notes in Computer Science, pages 51–67. Springer-Verlag, 1984. Full version in Information and Computation, 76(2/3):138–164, 1988.

Cardelli, Luca. Amber. In Guy Cousineau, Pierre-Louis Curien, and Bernard Robinet, editors, Combinators and Functional Programming Languages, pages 21–47. Springer-Verlag, 1986. Lecture Notes in Computer Science No. 242.

Cardelli, Luca. Basic polymorphic typechecking. Science of Computer Programming, 8(2):147–172, April 1987. An earlier version appeared in the Polymorphism Newsletter, January, 1985.

Cardelli, Luca. Structural subtyping and the notion of power type. In ACM Symposium on Principles of Programming Languages (POPL), San Diego, California, pages 70–79, January 1988a.

Cardelli, Luca. Typechecking dependent types and subtypes. In M. Boscarol, L. Carlucci Aiello, and G. Levi, editors, Foundations of Logic and Functional Programming, Workshop Proceedings, Trento, Italy, (Dec. 1986), volume 306 of Lecture Notes in Computer Science, pages 45–57. Springer-Verlag 1988b.

Cardelli, Luca. Notes about . Unpublished manuscript, October 1990.

Cardelli, Luca. Typeful programming. In E. J. Neuhold and M. Paul, editors, Formal Description of Programming Concepts. Springer-Verlag, 1991. An earlier version appeared as DEC/Compaq Systems Research Center Research Report #45, February 1989.

Cardelli, Luca. Extensible records in a pure calculus of subtyping. Research report 81, DEC/Compaq Systems Research Center, January 1992. Also in Carl A. Gunter and John C. Mitchell, editors, Theoretical Aspects of Object-Oriented Programming: Types, Semantics, and Language Design (MIT Press, 1994).

Cardelli, Luca. An implementation of F_<:. Research report 97, DEC/Compaq Systems Research Center, February 1993.

Cardelli, Luca. Type systems. In Allen B. Tucker, editor, Handbook of Computer Science and Engineering. CRC Press, 1996.

Cardelli, Luca, James Donahue, Lucille Glassman, Mick Jordan, Bill Kalsow, and Greg Nelson. Modula-3 report (revised). Research report 52, DEC/Compaq Systems Research Center, November 1989.

Cardelli, Luca and Xavier Leroy. Abstract types and the dot notation. In Proceedings of the IFIP TC2 Working Conference on Programming Concepts and Methods. North Holland, 1990. Also appeared as DEC/Compaq SRC technical report 56.

Cardelli, Luca and Giuseppe Longo. A semantic basis for Quest. Journal of Functional Programming, 1(4):417–458, October 1991. Summary in ACM Conference on Lisp and Functional Programming, June 1990. Also available as DEC/Compaq SRC Research Report 55, Feb. 1990.

Cardelli, Luca, Simone Martini, John C. Mitchell, and Andre Scedrov. An extension of System F with subtyping. Information and Computation, 109(1–2):4–56, 1994. Summary in TACS '91 (Sendai, Japan,pp. 750–770).

Cardelli, Luca and John Mitchell. Operations on records. Mathematical Structures in Computer Science, 1:3–48, 1991. Also in Carl A. Gunter and John C. Mitchell, editors, Theoretical Aspects of Object-Oriented Programming: Types, Semantics, and Language Design (MIT Press, 1994); available as DEC/Compaq Systems Research Center Research Report #48, August, 1989, and in the proceedings of MFPS '89, Springer LNCS volume 442.

Cardelli, Luca and Peter Wegner. On understanding types, data abstraction, and polymorphism. Computing Surveys, 17(4):471–522, December 1985.

Cardone, Felice. Relational semantics for recursive types and bounded quantification. In Proceedings of the Sixteenth International Colloquium on Automata, Languages, and Programming, volume 372 of Lecture Notes in Computer Science, pages 164–178, Stresa, Italy, July 1989. Springer-Verlag.

Cardone, Felice and Mario Coppo. Type inference with recursive types: Syntax and semantics. Information and Computation, 92(1):48–80, 1991.

Cartwright, Robert and Guy L. Steele, Jr. Compatible genericity with run-time types for the Java programming language. In Craig Chambers, editor, ACM Symposium on Object Oriented Programming: Systems, Languages, and Applications (OOPSLA), Vancouver, British Columbia, SIGPLAN Notices 33(10), pages 201–215. ACM, October 1998.

Castagna, Giuseppe. Object-Oriented Programming: A Unified Foundation. Springer-Verlag, 1997.

Castagna, Giuseppe, Giorgio Ghelli, and Giuseppe Longo. A calculus for over-loaded functions with subtyping. Information and Computation, 117(1):115–135, 15 February 1995. preliminary version in LISP and Functional Programming, July 1992 (pp. 182–192), and as Rapport de Recherche LIENS-92-4, Ecole Normale Sup rieure, Paris.

Chambers, Craig. Object-oriented multi-methods in Cecil. In European Conference on Object-Oriented Programming (ECOOP), pages 33–56, 1992.

Chambers, Craig. The Cecil language: Specification and rationale. Technical report, University of Washington, March 1993.

Chambers, Craig and Gary Leavens. Type-checking and modules for multi-methods. In ACM Symposium on Object Oriented Programming: Systems, Languages, and Applications (OOPSLA), October 1994. SIGPLAN Notices 29(10).

Chen, Gang and Giuseppe Longo. Subtyping parametric and dependent types. In Kamareddine et al., editor,Type Theory and Term Rewriting, September 1996. Invited lecture.

Chirimar, Jawahar, Carl A. Gunter, and Jon G. Riecke. Reference counting as a computational interpretation of linear logic. Journal of Functional Programming, 6(2): 195–244, March 1996.

Church, Alonzo. An unsolvable problem of elementary number theory. American Journal of Mathematics, 58:354–363, 1936.

Church, Alonzo. A formulation of the simple theory of types. Journal of Symbolic Logic, 5:56–68, 1940.

Church, Alonzo. The Calculi of Lambda Conversion. Princeton University Press, 1941.

Clement, Dominique, Joelle Despeyroux, Thierry Despeyroux, and Gilles Kahn. A simple applicative language: Mini-ML. In ACM Conference on LISP and Functional Programming, pages 13–27, 1986.

Clinger, William, Daniel P. Friedman, and Mitchell Wand. A scheme for a higher-level semantic algebra. In John Reynolds and Maurice Nivat, editors, Algebraic Methods in Semantics, pages 237–250. Cambridge University Press, 1985.

Colazzo, Dario and Giorgio Ghelli. Subtyping recursive types in Kernel Fun. In 14th Symposium on Logic in Computer Science (LICS'99), pages 137–146. IEEE, July 1999.

Compagnoni, Adriana and Healfdene Goguen. Decidability of higher-order subtyping via logical relations,December 1997a. Manuscript, available at ftp://www.dcs.ed.ac.uk/pub/hhg/hosdec.ps.gz.

Compagnoni, Adriana and Healfdene Goguen. Typed operational semantics for higher order subtyping. Technical Report ECS-LFCS-97-361, University of Edinburgh, July 1997b.

Compagnoni, Adriana B. Decidability of higher-order subtyping with intersection types. In Computer Science Logic, September 1994. Kazimierz, Poland. Springer Lecture Notes in Computer Science 933, June 1995. Also available as University of Edinburgh, LFCS technical report ECS-LFCS-94-281, titled "Subtyping in is decidable".

Compagnoni, Adriana B. and Benjamin C. Pierce. Intersection types and multiple inheritance. Mathematical Structures in Computer Science, 6(5):469–501, October 1996. Preliminary version available as University of Edinburgh technical report ECS-LFCS-93-275 and Catholic University Nijmegen computer science technical report 93-18, Aug. 1993, under the title "Multiple Inheritance via Intersection Types".

Constable, Robert L. Types in computer science, philosophy, and logic. In Samuel R. Buss, editor, Handbook of Proof Theory, volume 137 of Studies in logic and the foundations of mathematics, pages 683–786. Elsevier, 1998.

Constable et al., Robert L. Implementing Mathematics with the NuPRL Proof Development System. Prentice-Hall, Englewood Cliffs, NJ, 1986.

Cook, William. Object-oriented programming versus abstract data types. In J. W. de Bakker et al., editors, Foundations of Object-Oriented Languages, volume 489 of Lecture Notes in Computer Science, pages 151–178. Springer-Verlag, 1991.

Cook, William and Jens Palsberg. A denotational semantics of inheritance and its correctness. In ACM Symposium on Object Oriented Programming: Systems, Languages, and Applications (OOPSLA), pages 433–444, 1989.

Cook, William R. A Denotational Semantics of Inheritance. PhD thesis,.Brown University, 1989.

Cook, William R., Walter L. Hill, and Peter S. Canning. Inheritance is not subtyping. In ACM Symposium on Principles of Programming Languages (POPL), San Francisco, California, pages 125–135, January 1990. Also in Carl A. Gunter and John C. Mitchell, editors, Theoretical Aspects of Object-Oriented Programming: Types, Semantics, and Language Design (MIT Press, 1994).

Coppo, Mario and Mariangiola Dezani-Ciancaglini. A new type-assignment for λ-terms. Archiv Math. Logik, 19:139–156, 1978.

Coppo, Mario, Mariangiola Dezani-Ciancaglini, and Patrick Sall . Functional characterization of some semantic equalities inside λ-calculus. In Hermann A. Maurer, editor, Proceedings of the 6th Colloquium on Automata, Languages and Programming, volume 71 of LNCS, pages 133–146, Graz, Austria, July 1979. Springer.

Coquand, Thierry. Une Th orie des Constructions. PhD thesis, University Paris VII, January 1985.

Coquand, Thierry and G rard Huet. The Calculus of Constructions. Information and Computation, 76(2/3):95–120, February/March 1988.

Courcelle, Bruno. Fundamental properties of infinite trees. Theoretical Computer Science, 25:95–169, 1983.

Cousineau, Guy and Michel Mauny. The Functional Approach to Programming. Cambridge University Press, 1998.

Crary, Karl. Sound and complete elimination of singleton kinds. Technical Report CMU-CS-00-104, Carnegie Mellon University, School of Computer Science,January 2000.

Crary, Karl, Robert Harper, and Derek Dreyer. A type system for higher-order modules. In ACM Symposium on Principles of Programming Languages (POPL), Portland, Oregon, 2002.

Crary, Karl, Robert Harper, and Sidd Puri. What is a recursive module? In ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), pages 50–63, May 1999.

Crary, Karl, Stephanie Weirich, and J. Gregory Morrisett. Intensional polymorphism in type-erasure semantics. In International Conference on Functional Programming (ICFP), Baltimore, Maryland, USA, pages 301–312, 1998.

Crole, Roy. Categories for Types. Cambridge University Press, 1994.

Curien, Pierre-Louis and Giorgio Ghelli. Subtyping + extensionality: Confluence of βη-reductions in F_≤. In T. Ito and A. R. Meyer, editors, Theoretical Aspects of Computer Software (Sendai, Japan), number 526 in Lecture Notes in Computer Science, pages 731–749. Springer-Verlag, September 1991.

Curien, Pierre-Louis and Giorgio Ghelli. Coherence of subsumption: Minimum typing and type-checking in F_≤. Mathematical Structures in Computer Science, 2:55–91, 1992. Also in Carl A. Gunter and John C. Mitchell, editors, Theoretical Aspects of Object-Oriented Programming: Types, Semantics, and Language Design (MIT Press, 1994).

Curry, Haskell B. and Robert Feys. Combinatory Logic, volume 1. North Holland, 1958. Second edition,1968.

Damas, Luis and Robin Milner. Principal type schemes for functional programs. In ACM Symposium on Principles of Programming Languages (POPL), Albuquerque,New Mexico, pages 207–212, 1982.

Danvy, Olivier. Type-directed partial evaluation. In John Hatcliff, Torben . Mogensen, and Peter Thiemann, editors, Partial Evaluation - Practice and Theory; Proceedings of the 1998 DIKU Summer School, number 1706 in Lecture Notes in Computer Science, pages 367–411, Copenhagen, Denmark, July 1998. Springer-Verlag.

Davey, Brian A. and Hilary A. Priestley. Introduction to Lattices and Order. Cambridge University Press, 1990.

Davies, Rowan. A refinement-type checker for Standard ML. In International Conference on Algebraic Methodology and Software Technology, volume 1349 of Lecture Notes in Computer Science. Springer-Verlag, 1997.

Davies, Rowan and Frank Pfenning. A modal analysis of staged computation. In ACM Symposium on Principles of Programming Languages (POPL), St. Petersburg Beach, Florida, pages 258–270, 1996.

de Bruijn, Nicolas G. Lambda-calculus notation with nameless dummies: a tool for automatic formula manipulation with application to the Church-Rosser theorem. Indag. Math., 34(5):381–392, 1972.

de Bruijn, Nicolas G. A survey of the project AUTOMATH.In J. P. Seldin and J. R. Hindley, editors, To H. B. Curry: Essays in Combinatory Logic, Lambda Calculus, and Formalism, pages 589–606. Academic Press, 1980.

De Millo, Richard A., Richard J. Lipton, and Alan J. Perlis. Social processes and proofs of theorems and programs. Communications of the ACM, 22(5):271–280, May 1979. An earlier version appeared in ACM Symposium on Principles of Programming Languages (POPL), Los Angeles, California, 1977pp. 206–214.

Detlefs, David L., K. Rustan M. Leino, Greg Nelson, and James B. Saxe. Extended static checking. Technical Report 159, Compaq Systems Research Center (SRC), 1998. Also see http://research.compaq.com/SRC/esc/overview.html.

Donahue, James and Alan Demers. Data types are values. ACM Transactions on Programming Languages and Systems, 7(3):426–445, July 1985.

Dowek, Gilles, Th r se Hardin, Claude Kirchner, and Frank Pfenning. Unification via explicit substitutions: The case of higher-order patterns. In M. Maher, editor, Proceedings of the Joint International Conference and Symposium on Logic Programming, pages 259–273, Bonn, Germany, September 1996. MIT Press.

Drossopoulou, Sophia, Susan Eisenbach, and Sarfraz Khurshid. Is the Java Type System Sound?Theory and Practice of Object Systems, 7(1):3–24, 1999. Summary in European Conference on Object-Oriented Programming (ECOOP), 1997.

Duggan, Dominic and Adriana Compagnoni. Subtyping for object type constructors. In Workshop on Foundations of Object-Oriented Languages (FOOL), informal proceedings, January 1999.

Dybvig, R. Kent. The Scheme Programming Language. Prentice-Hall, Inc., Englewood Cliffs, New Jersey, second edition,1996. Available electronically at http://www.scheme.com/tsp12d/

Eidorff, Peter, Fritz Henglein, Christian Mossin, Henning Niss, Morten Heine B. S rensen, and Mads Tofte. AnnoDomini in practice: A type-theoretic approach to the Year 2000 problem. In Jean-Yves Girard, editor, Proc. Symposium on Typed Lambda Calculus and Applications (TLCA), volume 1581 of Lecture Notes in Computer Science, pages 6–13, L'Aquila, Italy, April 1999. Springer-Verlag.

Eifrig, Jonathan, Scott Smith, and Valery Trifonov. Type inference for recursively constrained types and its application to OOP. In Proceedings of the 1995 Mathematical Foundations of Programming Semantics Conference, volume 1 of Electronic Notes in Theoretical Computer Science. Elsevier, 1995.

Feinberg, Neal, Sonya E. Keene, Robert O. Mathews, and P. Tucker Withington. The Dylan Programming Book. Addison-Wesley Longman, Reading, Mass., 1997.

Felleisen, Matthias and Daniel P. Friedman. A Little Java, A Few Patterns. MIT Press, Cambridge, Massachusetts, 1998.

Felty, Amy, Elsa Gunter, John Hannan, Dale Miller, Gopalan Nadathur, and Andre Scedrov. Lambda prolog: An extended logic programming language. In E. Lusk; R. Overbeek, editor, Proceedings on the 9th International Conference on Automated Deduction, volume 310 of LNCS, pages 754–755, Berlin, May 1988. Springer.

Filinski, Andrzej. A semantic account of type-directed partial evaluation. In Gopalan Nadathur, editor, Proceedings of the International Conference on Principles and Practice of Declarative Programming, number 1702 in Lecture Notes in Computer Science, pages 378–395, Paris, France, September 1999. Springer-Verlag. Extended version available as technical report BRICS RS-99-17.

Filinski, Andrzej. Normalization by evaluation for the computational lambda-calculus. In Samson Abramsky, editor, Typed Lambda Calculi and Applications, 5th International Conference, TLCA 2001, number 2044 in Lecture Notes in Computer Science, pages 151–165, Krak w, Poland, May 2001. Springer-Verlag.

Fisher, Kathleen. Classes = objects + data abstraction. In Kim Bruce and Giuseppe Longo, editors, Workshop on Foundations of Object-Oriented Languages (FOOL), informal proceedings, July 1996a. Invited talk. Also available as Stanford University Technical Note STAN-CS-TN-96-31.

Fisher, Kathleen. Type Systems for object-oriented programming languages. PhD thesis, Stanford University,1996b. STAN-CS-TR-98-1602.

Fisher, Kathleen, Furio Honsell, and John C. Mitchell. A lambda calculus of objects and method specialization. Nordic J. Computing (formerly BIT), 1:3–37, 1994. Summary in Proc. IEEE Symp. on Logic in Computer Science, 1993, 26–38.

Fisher, Kathleen and John Mitchell. The development of type systems for object-oriented languages. Theory and Practice of Object Systems, 1(3):189–220, 1996.

Fisher, Kathleen and John C. Mitchell. On the relationship between classes, objects, and data abstraction. Theory and Practice of Object Systems, 4(1):3–25, 1998.

Fisher, Kathleen and John H. Reppy. The design of a class mechanism for Moby. In SIGPLAN Conference on Programming Language Design and Implementation (PDLI), pages 37–49, 1999.

Flanagan, Cormac and Matthias Felleisen. Componential set-based analysis. ACM SIGPLAN Notices, 32(5):235–248, May 1997.

Flatt, Matthew and Matthias Felleisen. Units: Cool modules for HOT languages. In ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), Montreal, Canada, pages 236–248, 1998.

Flatt, Matthew, Shriram Krishnamurthi, and Matthias Felleisen. Classes and mixins. In ACM Symposium on Principles of Programming Languages (POPL), San Diego, California, January 1998a.

Flatt, Matthew, Shriram Krishnamurthi, and Matthias Felleisen. A programmer's reduction semantics for classes and mixins. Technical Report TR97-293, Computer Science Department, Rice University,February 1998b. Corrected June, 1999.

Freeman, Tim and Frank Pfenning. Refinement types for ML. In ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), Toronto, Ontario, June 1991.

Frege, Gottlob. Beagriffschrift, eine der arithmetischen nachgebildete Formelsprache des reinen Denkens. Halle: L. Nebert, 1879. Available in several translations.

Friedman, Daniel P. and Matthias Felleisen. The Little Schemer. MIT Press, 1996.

Friedman, Daniel P., Mitchell Wand, and Christopher T. Haynes. Essentials of Programming Languages. McGraw-Hill Book Co., New York, N.Y.,second edition, 2001.

Friedman, Harvey. Equality between functionals. In Rohit Parikh, editor, Logic Colloquium, volume 453 of Lecture Notes in Mathematics, pages 22–37, Berlin, 1975. Springer-Verlag.

Gallier, Jean. On Girard's "Candidats de reductibilit ". In Piergiorgio Odifreddi, editor, Logic and Computer Science, number 31 in APIC Studies in Data Processing, pages 123–203. Academic Press, 1990.

Gallier, Jean. Constructive logics. Part I: A tutorial on proof systems and typed λ-calculi. Theoretical Computer Science, 110(2):249–339, March 1993.

Gandy, Robin O. The simple theory of types. In Logic Colloquium 76, volume 87 of Studies in Logic and the Foundations of Mathematics, pages 173–181. North Holland, 1976.

Gapeyev, Vladimir, Michael Levin, and Benjamin Pierce. Recursive subtyping revealed. In International Conference on Functional Programming (ICFP), Montreal, Canada, 2000. To appear in Journal of Functional Programming.

Garrigue, Jaques and Hassan A t-Kaci. The typed polymorphic label-selective lambda-calculus. In ACM Symposium on Principles of Programming Languages (POPL), Portland, Oregon, pages 35–47, 1994.

Garrigue, Jaques and Didier R my. Extending ML with semi-explicit polymorphism. In Mart n Abadi and Takayasu Ito, editors, International Symposium on Theoretical Aspects of Computer Software (TACS), Sendai, Japan, pages 20–46. Springer-Verlag, September 1997.

Ghelli, Giorgio. Proof Theoretic Studies about a Minimal Type System Integrating Inclusion and Parametric Polymorphism. PhD thesis, Universit di Pisa, March 1990. Technical report TD-6/90, Dipartimento di Informatica, Universit di Pisa.

Ghelli, Giorgio. Recursive types are not conservative over F_≤. In M. Bezen and J.F. Groote, editors, Typed Lambda Calculi and Applications (TLCA), Utrecht, The Netherlands, number 664 in Lecture Notes in Computer Science, pages 146–162, Berlin, March 1993. Springer-Verlag.

Ghelli, Giorgio. Divergence of F_≤ type checking. Theoretical Computer Science, 139 (1,2):131–162, 1995.

Ghelli, Giorgio. Termination of system F-bounded: A complete proof. Information and Computation, 139(1):39–56, 1997.

Ghelli, Giorgio and Benjamin Pierce. Bounded existentials and minimal typing. Theoretical Computer Science, 193:75–96, 1998.

Gifford, David, Pierre Jouvelot, John Lucassen, and Mark Sheldon. FX-87 Reference Manual. Technical Report MIT/LCS/TR-407, Massachusetts Institute of Technology, Laboratory for Computer Science, September 1987.

Girard, Jean-Yves. Interpr tation fonctionnelle et limination des coupures de l'arithm tique d'ordre sup rieur. Th se d' tat, Universit Paris VII, 1972. Summary in Proceedings of the Second Scandinavian Logic Symposium (J.E. Fenstad, editor), North-Holland, 1971(pp. 63–92).

Girard, Jean-Yves. Linear logic. Theoretical Computer Science, 50:1–102, 1987.

Girard, Jean-Yves, Yves Lafont, and Paul Taylor. Proofs and Types, volume 7 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 1989.

Glew, Neal. Type dispatch for named hierarchical types. In International Conference on Functional Programming (ICFP), Paris, France,pages 172–182, 1999.

Gordon, Andrew. A tutorial on co-induction and functional programming. In Functional Programming, Glasgow 1994, pages 78–95. Springer Workshops in Computing, 1995.

Gordon, Michael J. Adding eval to ML. Manuscript, circa 1980.

Gordon, Michael J., Robin Milner, and Christopher P. Wadsworth. Edinburgh LCF. Springer-Verlag LNCS 78, 1979.

Goto, Eiichi. Monocopy and associative algorithms in extended Lisp. Technical Report TR 74-03, University of Tokyo,May 1974.

Goubault-Larrecq, Jean and Ian Mackie. Proof Theory and Automated Deduction (Applied Logic Series, V. 6). Kluwer, 1997.

Grattan-Guinness, Ivor. The search for mathematical roots, 1870–1940: Logics, set theories and the foundations of mathematics from Cantor through Russell to G del. Princeton University Press, 2001.

Gries, David, editor.Programming Methodology. Springer-Verlag, New York, 1978.

Gunter, Carl A. Semantics of Programming Languages: Structures and Techniques. MIT Press, 1992.

Gunter, Carl A. and John C. Mitchell. Theoretical Aspects of Object-Oriented Programming: Types, Semantics, and Language Design. MIT Press, 1994.

Hall, Cordelia V., Kevin Hammond, Simon L. Peyton Jones, and Philip L. Wadler. Type classes in Haskell. ACM Transactions on Programming Languages and Systems, 18 (2):109–138, March 1996.

Halmos, Paul R. Naive Set Theory. Springer, New York, 1987.

Harper, Robert. A simplified account of polymorphic references. Information Processing Letters, 51(4):201–206, August 1994. See also (Harper, 1996).

Harper, Robert. A note on: "A simplified account of polymorphic references" [Inform. Process. Lett. 51 (1994), no. 4, 201–206; MR 95f:68142]. Information Processing Letters, 57(1):15–16, January 1996. See (Harper, 1994).

Harper, Robert, Bruce Duba, and David MacQueen. First-class continuations in ML. Journal of Functional Programming, 3(4), October 1993. Short version in POPL '91.

Harper, Robert, Furio Honsell, and Gordon Plotkin. A framework for defining logics. Journal of the ACM, 40(1):143–184, 1992. Summary in LICS'87.

Harper, Robert and Mark Lillibridge. A type-theoretic approach to higher-order modules with sharing. In ACM Symposium on Principles of Programming Language (POPL), Portland, Oregon, pages 123–137, January 1994.

Harper, Robert, John C. Mitchell, and Eugenio Moggi. Higher-order modules and the phase distinction. In ACM Symposium on Principles of Programming Languages (POPL), San Francisco, California, pages 341–354, January 1990.

Harper, Robert and Greg Morrisett. Compiling polymorphism using intensional type analysis. In ACM Symposium on Principles of Programming Languages (POPL), San Francisco, California, pages 130–141, 1995.

Harper, Robert and Benjamin Pierce. A record calculus based on symmetric concatenation. In ACM Symposium on Principles of Programming Languages (POPL), Orlando, Florida, pages 131–142, January 1991. Extended version available as Carnegie Mellon Technical Report CMU-CS-90-157.

Harper, Robert and Christopher Stone. A type-theoretic interpretation of Standard ML. In Gordon Plotkin, Colin Stirling, and Mads Tofte, editors, Proof, Language and Interaction: Essays in Honour of Robin Milner. MIT Press, 2000.

Hasegawa, Ryu. Parametricity of extensionally collapsed term models of polymorphism and their categorical properties. In Takayasu Ito and Albert Meyer, editors, Theoretical Aspects of Computer Software (TACS), Sendai, Japan, 1991.

Hayashi, Susumu. Singleton, union and intersection types for program extraction. In T. Ito and A. R. Meyer, editors, Theoretical Aspects of Computer Software (Sendai, Japan), number 526 in Lecture Notes in Computer Science, pages 701–730. Springer-Verlag, September 1991. Full version in Information and Computation, 109(1/2):174–210, 1994.

Henglein, Fritz. Type inference with polymorphic recursion. ACM Transactions on Programming Languages and Systems, 15(2):253–289, 1993.

Henglein, Fritz. Dynamic typing: syntax and proof theory. Science of Computer Programming, 22(3):197–230, June 1994. Selected papers of the Fourth European Symposium on Programming (Rennes, 1992).

Henglein, Fritz and Harry G. Mairson. The complexity of type inference for higher-order typed lambda-calculi. In ACM Symposium on Principles of Programming Languages (POPL), Orlando, Florida, pages 119–130, January 1991.

Hennessy, Matthew. A Semantics of Programming Languages: An Elementary Introduction Using Operational Semantics. John Wiley and Sons, 1990. Currently out of print; available from http://www.cogs.susx.ac.uk/users/matthewh/semnotes.ps.gz.

Hennessy, Matthew and James Riely. Resource access control in systems of mobile agents. In Uwe Nestmann and Benjamin C. Pierce, editors, HLCL '98: High-Level Concurrent Languages (Nice, France, September 12, 1998),volume 16.3 of ENTCS, pages 3–17. Elsevier Science Publishers, 1998. Full version available as CogSci Report 2/98, University of Sussex,Brighton.

Hindley, J. Roger. The principal type-scheme of an object in combinatory logic. Transaction of the American Mathematical Society, 146:29–60, 1969.

Hindley, J. Roger. Types with intersection, an introduction. Formal Aspects of Computing, 4:470–486, 1992.

Hindley, J. Roger. Basic Simple Type Theory, volume 42 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, Cambridge 1997.

Hindley, J. Roger and Jonathan P. Seldin. Introduction to Combinators and λ-Calculus, volume 1 of London Mathematical Society Student Texts. Cambridge University Press, 1986.

Hoang, My, John Mitchell, and Ramesh Viswanathan. Standard ML-NJ weak polymorphism and imperative constructs. In Proceedings, Eighth Annual IEEE Symposium on Logic in Computer Science, pages 15–25. IEEE Computer Society Press, 1993.

Hodas, J. S. Lolli: An extension of λProlog with linear context management. In D. Miller, editor, Workshop on the λProlog Programming Language, pages 159–168, Philadelphia, Pennsylvania, August 1992.

Hofmann, Martin. Syntax and semantics of dependent types. In Semantics and Logic of Computation. Cambridge University Press, 1997.

Hofmann, Martin and Benjamin Pierce. Positive subtyping. In ACM Symposium on Principles of Programming Languages (POPL), San Francisco, California, pages 186–197, January 1995a. Full version in Information and Computation, volume 126, number 1, April 1996. Also available as University of Edinburgh technical report ECS-LFCS-94-303, September 1994.

Hofmann, Martin and Benjamin Pierce. A unifying type-theoretic framework for objects. Journal of Functional Programming, 5(4):593–635, October 1995b. Previous versions appeared in the Symposium on Theoretical Aspects of Computer Science, 1994, (pages 251–262) and, under the title "An Abstract View of Objects and Subtyping (Preliminary Report)," as University of Edinburgh, LFCS technical report ECS-LFCS-92-226, 1992.

Hofmann, Martin and Benjamin C. Pierce. Type destructors. In Didier R my, editor, Informal proceedings of the Fourth International Workshop on Foundations of Object-Oriented Languages (FOOL), January 1998. Full version to appear in Information and Computation.

Hook, J.G. Understanding Russell - a first attempt. In Proc. Int. Symp. on Semantics of Data Types, Sophia-Antipolis (France), Springer LNCS 173, pages 69–85. Springer-Verlag, 1984.

Hopcroft, John E. and Jeffrey D. Ullman. Introduction to Automata Theory, Languages, and Computation. Addison-Wesley, 1979.

Hosoya, Haruo and Benjamin Pierce. Regular expression pattern matching. In ACM Symposium on Principles of Programming Languages (POPL), London, England,2001.

Hosoya, Haruo and Benjamin C. Pierce. How good is local type inference? Technical Report MS-CIS-99-17, University of Pennsylvania,June 1999.

Hosoya, Haruo and Benjamin C. Pierce. XDuce: A typed XML processing language (preliminary report). In International Workshop on the Web and Databases (WebDB), May 2000.

Hosoya, Haruo, J r me Vouillon, and Benjamin C. Pierce. Regular expression types for XML. ACM Transactions on Programming Languages and Systems (TOPLAS), 2001. To appear; short version in ICFP 2000.

Howard, William A. Hereditarily majorizable functionals of finite type. In Anne Sjerp Troelstra, editor, Metamathematical Investigation of Intuitionistic Arithmetic and Analysis, volume 344 of Lecture Notes in Mathematics, pages 454–461. Springer-Verlag, Berlin, 1973. Appendix.

Howard, William A. The formulas-as-types notion of construction. In J. P. Seldin and J. R. Hindley, editors, To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus, and Formalism, pages 479–490. Academic Press, New York, 1980. Reprint of 1969 article.

Howe, Douglas. Automating Reasoning in an Implementation of Constructive Type Theory. PhD thesis, Cornell University,1988.

Hudak, Paul, S. Peyton Jones, P. Wadler, B. Boutel, J. Fairbairn, J. Fasel, M. M. Guzman, K. Hammond, J. Hughes, T. Johnsson, D. Kieburtz, R. Nikhil, W. Partain, and J. Peterson. Report on the programming language Haskell, version 1.2. SIGPLAN Notices, 27(5), May 1992.

Huet, G rard. A unification algorithm for typed λ-calculus. Theoretical Computer Science, 1:27–57, 1975.

Huet, G rard. R solution d'equations dans les langages d'ordre 1,2, …,ω. Th se de Doctorat d'Etat, Universit de Paris 7(France), 1976.

Huet, G rard, editor. Logical Foundations of Functional Programming. University of Texas at Austin Year of Programming Series.Addison-Wesley, 1990.

Hyland, J. Martin E. and C.-H. Luke Ong. On full abstraction for PCF: I, II, and III. Information and Computation, 163(2):285–408, December 2000.

Igarashi, Atsushi, Benjamin Pierce, and Philip Wadler. Featherweight Java: A minimal core calculus for Java and GJ. In ACM Symposium on Object Oriented Programming: Systems, Languages, and Applications (OOPSLA), October 1999. Full version to appear in ACM Transactions on Programming Languages and Systems (TOPLAS), 2001.

Igarashi, Atsushi and Benjamin C. Pierce. On inner classes. In European Conference on Object-Oriented Programming (ECOOP), 2000. Also in informal proceedings of the Seventh International Workshop on Foundations of Object-Oriented Languages (FOOL). To appear in Information and Computation.

Igarashi, Atsushi, Benjamin C. Pierce, and Philip Wadler. A recipe for raw types. In Workshop on Foundations of Object-Oriented Languages (FOOL), 2001.

Ishtiaq, Samin and Peter O'Hearn. Bi as an assertion language for mutable data structures. In ACM Symposium on Principles of Programming Languages (POPL), London, England,2001.

Jacobs, Bart. Categorical Logic and Type Theory. Number 141 in Studies in Logic and the Foundations of Mathematics.North Holland, Elsevier, 1999.

Jagannathan, Suresh and Andrew Wright. Effective flow analysis for avoiding run-time checks. In Proceedings of the Second International Static Analysis Symposium, volume 983 of LNCS, pages 207–224. Springer-Verlag, 1995.

Jay, C. Barry and Milan Sekanina. Shape checking of array programs. In Computing: The Australasian Theory Seminar (Proceedings), volume 19 of Australian Computer Science Communications, pages 113–121, 1997.

Jim, Trevor. Rank-2 type systems and recursive definitions. Technical Report MIT/LCS/TM-531, Massachusetts Institute of Technology, Laboratory for Computer Science, November 1995.

Jim, Trevor. What are principal typings and what are they good for? In ACM, editor,ACM Symposium on Principles of Programming Languages (POPL), St. Petersburg Beach, Florida, pages 42–53, 1996.

Jim, Trevor and Jens Palsberg. Type inference in systems of recursive types with subtyping. Manuscript, 1999.

Jones, Mark P. ML typing, explicit polymorphism, and qualified types,1994a.

Jones, Mark P. Qualified Types: Theory and Practice. Cambridge University Press, 1994b.

Jones, Richard and Rafael D. Lins. Garbage Collection: Algorithms for Automatic Dynamic Memory Management. Wiley, 1996.

Jouvelot, Pierre and David Gifford. Algebraic reconstruction of types and effects. In ACM Symposium on Principles of Programming Languages (POPL), Orlando,Florida, pages 303–310, January 1991.

Jutting, L.S. van Benthem, James McKinna, and Robert Pollack. Checking algorithms for Pure Type Systems. In Henk Barendregt and Tobias Nipkow, editors, Proceedings of the International Workshop on Types for Proofs and Programs, pages 19–61, Nijmegen, The Netherlands, May 1994. Springer-Verlag LNCS 806.

Kaes, Stefan. Parametric overloading in polymorphic programming languages. In H. Ganzinger, editor, Proceedings of the European Symposium on Programming, volume 300 of Lecture Notes in Computer Science, pages 131–144. Springer-Verlag, 1988.

Kahn, Gilles. Natural semantics. In Proceedings of the Symposium on Theoretical Aspects of Computer Science (STACS), volume 247 of Lecture Notes in Computer Science, pages 22–39. Springer-Verlag, 1987.

Kamin, Samuel N. Inheritance in Smalltalk-80: A denotational definition. In ACM Symposium on Principles of Programming Languages (POPL), San Diego, California, pages 80–87, January 1988.

Kamin, Samuel N. and Uday S. Reddy. Two semantic models of object-oriented languages. In Carl A. Gunter and John C. Mitchell, editors, Theoretical Aspects of Object-Oriented Programming: Types, Semantics, and Language Design, pages 464–495. MIT Press, 1994.

Katiyar, Dinesh, David Luckham, and John Mitchell. A type system for prototyping languages. In ACM Symposium on Principles of Programming Languages (POPL), Portland, Oregon, pages 138–150, January 1994.

Katiyar, Dinesh and Sriram Sankar. Completely bounded quantification is decidable. In Proceedings of the ACM SIGPLAN Workshop on ML and its Applications, June 1992.

Kelsey, Richard, William Clinger, and Jonathan Rees. Revised⁵ report on the algorithmic language Scheme. Higher-Order and Symbolic Computation, 11(1):7–105, 1998. Also appears in ACM SIGPLAN Notices 33(9), September 1998.

Kennedy, Andrew. Dimension types. In Donald Sannella, editor, Programming Languages and Systems—ESOP'94, 5th European Symposium on Programming, volume 788 of Lecture Notes in Computer Science, pages 348–362, Edinburgh, U.K., 11–13 April 1994. Springer.

Kernighan, Brian W. and Dennis M. Ritchie. The C Programming Language. Prentice Hall, Englewood Cliffs, second edition,1988.

Kfoury, Assaf J., Harry Mairson, Franklyn Turbak, and Joe B. Wells. Relating typability and expressiveness in finite-rank intersection type systems. In International Conference on Functional Programming (ICFP), Paris, France, volume 34.9 of ACM Sigplan Notices, pages 90–101, N.Y., September 27–29 1999. ACM Press.

Kfoury, Assaf J. and Jerzy Tiuryn. Type reconstruction in finite-rank fragments of the polymorphic λ-calculus. In Fifth Annual IEEE Symposium on Logic in Computer Science, pages 2–11, Philadelphia, PA, June 1990. Full version in Information and Computation, 98(2), 228–257, 1992.

Kfoury, Assaf J., Jerzy Tiuryn, and Pawel Urzyczyn. ML typability is DEXPTIME-complete. In Proc. 15th Colloq. on Trees in Algebra and Programming, pages 206–220. Springer LNCS 431, 1990.

Kfoury, Assaf J., Jerzy Tiuryn, and Pawel Urzyczyn. Type reconstruction in the presence of polymorphic recursion. ACM Transactions on Programming Languages and Systems, 15(2):290–311, April 1993a.

Kfoury, Assaf J., Jerzy Tiuryn, and Pawel Urzyczyn. The undecidability of the semi-unification problem. Information and Computation, 102(1):83–101, January 1993b. Summary in STOC 1990.

Kfoury, Assaf J., Jerzy Tiuryn, and Pawel Urzyczyn. An analysis of ML typability. Journal of the ACM, 41(2):368–398, March 1994.

Kfoury, Assaf J. and Joe B. Wells. Principality and decidable type inference for finite-rank intersection types. In ACM Symposium on Principles of Programming Languages (POPL), San Antonio, Texas, pages 161–174, New York, NY, January 1999. ACM.

Kiczales, Gregor, Jim des Rivi res, and Daniel G. Bobrow. The Art of the Metaobject Protocol. MIT Press, Cambridge, MA, 1991.

Kirchner, Claude and Jean-Pierre Jouannaud. Solving equations in abstract algebras: a rule-based survey of unification. Research Report 561, Universit de Paris Sud, Orsay, France, April 1990.

Klop, Jan W. Combinatory Reduction Systems. Mathematical Centre Tracts 127.Mathematisch Centrum, Amsterdam, 1980.

Kobayashi, Naoki, Benjamin C. Pierce, and David N. Turner. Linearity and the pi-calculus. In ACM Symposium on Principles of Programming Languages (POPL), St. Petersburg Beach,Florida, 1996. Full version in ACM Transactions on Programming Languages and Systems, 21(5), pp. 914–947, September 1999.

Kozen, Dexter, Jens Palsberg, and Michael I. Schwartzbach. Efficient recursive subtyping. In ACM Symposium on Principles of Programming Languages (POPL), Charleston, South Carolina, pages 419–428, 1993.

Laan, Twan Dismas Laurens. The Evolution of Type Theory in Logic and Mathematics. PhD thesis, Techn. Univ. Eindhoven, 1997.

Landin, Peter J. The mechanical evaluation of expressions. Computer Journal, 6: 308–320, January 1964.

Landin, Peter J. A correspondence between ALGOL 60 and Church's lambda-notation: Parts I and II. Communications of the ACM, 8(2,3):89–101, 158–165, February and March 1965.

Landin, Peter J. The next 700 programming languages. Communications of the ACM, 9(3):157–166, March 1966.

Lassez, Jean-Louis and Gordin Plotkin, editors.Computational Logic, Essays in Honor of Alan Robinson. MIT Press, 1991.

L ufer, Konstantin. Polymorphic Type Inference and Abstract Data Types. PhD thesis, New York University, 1992.

L ufer, Konstantin and Martin Odersky. Polymorphic type inference and abstract data types. ACM Transactions on Programming Languages and Systems (TOPLAS), 16(5):1411–1430, September 1994. Summary in Phoenix Seminar and Workshop on Declarative Programming, Nov. 1991.

League, Christopher, Zhong Shao, and Valery Trifonov. Representing Java classes in a typed intermediate language. In International Conference on Functional Programming (ICFP), Paris, France, September 1999.

League, Christopher, Valery Trifonov, and Zhong Shao. Type-preserving compilation of Featherweight Java. In Foundations of Object-Oriented Languages (FOOL8), London, January 2001.

Lee, Oukseh and Kwangkeun Yi. Proofs about a folklore let-polymorphic type inference algorithm. ACM Transactions on Programming Languages and Systems, 20 (4):707–723, July 1998.

Leivant, Daniel. Polymorphic type inference. In Proceedings of the 10th Annual ACM Symposium on Principles of Programming Languages. ACM, 1983.

Lemmon, E. John, Carew A. Meredith, David Meredith, Arthur N. Prior, and Ivo Thomas. Calculi of pure strict implication,1957. Mimeographed version, 1957; published in Philosophical Logic, ed. Davis, Hockney, and Wilson, D. Reidel Co., Netherlands, 1969, pp. 215–250.

Leroy, Xavier. Manifest types, modules and separate compilation. In ACM Symposium on Principles of Programming Languages (POPL), Portland, Oregon, pages 109–122, Portland, OR, January 1994.

Leroy, Xavier. The Objective Caml system: Documentation and user's manual,2000. With Damien Doligez, Jacques Garrigue, Didier R my, and J r me Vouillon. Available from http://caml.inria.fr.

Leroy, Xavier and Michel Mauny. Dynamics in ML. In John Hughes, editor, ACM Symposium on Functional Programming Languages and Computer Architecture (FPCA) 1991, volume 523 of Lecture Notes in Computer Science, pages 406–426. Springer-Verlag, 1991.

Leroy, Xavier and Fran ois Pessaux. Type-based analysis of uncaught exceptions. ACM Transactions on Programming Languages and Systems, 22(2):340–377, March 2000. Summary in ACM Symposium on Principles of Programming Languages (POPL), San Antonio, Texas, 1999.

Leroy, Xavier and Fran ois Rouaix. Security properties of typed applets. In ACM Symposium on Principles of Programming Languages (POPL), San Diego, California, pages 391–403, January 1998.

Leroy, Xavier and Pierre Weis. Polymorphic type inference and assignment. In ACM Symposium on Principles of Programming Languages (POPL), Orlando,Florida, pages 291–302, 1991.

Lescanne, Pierre and Jocelyn Rouyer-Degli. Explicit substitutions with de Bruijn's levels. In J. Hsiang, editor, Proceedings of the 6th Conference on Rewriting Techniques and Applications (RTA), Kaiserslautern (Germany), volume 914, pages 294–308, 1995.

Levin, Michael Y. and Benjamin C. Pierce. Tinkertype: A language for playing with formal systems. Journal of Functional Programming, 2001. To appear. A preliminary version appeared as an invited talk at the Logical Frameworks and Metalanguages Workshop (LFM), June 2000.

Lillibridge, Mark. Translucent Sums: A Foundation for Higher-Order Module Systems. PhD thesis, School of Computer Science, Carnegie Mellon University, Pittsburgh, PA, May 1997.

Liskov, Barbara, Russell Atkinson, Toby Bloom, Elliott Moss, J. Craig Schaffert, Robert Scheifler, and Alan Snyder. CLU Reference Manual. Springer-Verlag, 1981.

Liskov, Barbara, Alan Snyder, Russell Atkinson, and J. Craig Schaffert. Abstraction mechanisms in CLU. Communications of the ACM, 20(8):564–576, August 1977. Also in S. Zdonik and D. Maier, eds., Readings in Object-Oriented Database Systems.

Luo, Zhaohui. Computation and Reasoning: A Type Theory for Computer Science. Number 11 in International Series of Monographs on Computer Science. Oxford University Press, 1994.

Luo, Zhaohui and Robert Pollack. The LEGO proof development system: A user's manual. Technical Report ECS-LFCS-92-211, University of Edinburgh, May 1992.

Ma, QingMing. Parametricity as subtyping. In ACM Symposium on Principles of Programming Languages (POPL), Albuquerque, New Mexico, January 1992.

Mackie, Ian. Lilac: A functional programming language based on linear logic. Journal of Functional Programming, 4(4):395–433, October 1994.

MacQueen, David. Using dependent types to express modular structure. In ACM Symposium on Principles of Programming Languages (POPL), St. Petersburg Beach,Florida, pages 277–286, January 1986.

MacQueen, David, Gordon Plotkin, and Ravi Sethi. An ideal model for recursive polymorphic types. Information and Control, 71:95–130, 1986.

MacQueen, David B. Using dependent types to express modular structure. In ACM Symposium on Principles of Programming Languages (POPL), St. Petersburg Beach,Florida, 1986.

Magnusson, Lena and Bengt Nordstr m. The ALF proof editor and its proof engine. In Henk Barendregt and Tobias Nipkow, editors, Types for Proofs and Programs. pages 213–237. Springer-Verlag LNCS 806, 1994.

Mairson, Harry G. Deciding ML typability is complete for deterministic exponential time. In ACM Symposium on Principles of Programming Languages (POPL), San Francisco, California, pages 382–401. ACM Press, New York, 1990.

Martin-L f, Per. An intuitionistic theory of types: predicative part. In H. E. Rose and J. C. Shepherdson, editors, Logic Colloquium, '73, pages 73–118. North-Holland, Amsterdam, 1973.

Martin-L f, Per. Constructive mathematics and computer programming. In Logic, Methodology and Philosophy of Science, VI. North Holland, Amsterdam, 1982.

Martin-L f, Per. Intuitionistic Type Theory. Bibliopolis, 1984.

Martini, Simone. Bounded quantifiers have interval models. In Proceedings of the ACM Conference on Lisp and Functional Programming, pages 174–183, Snowbird, Utah, July 1988. ACM.

McCarthy, John. History of LISP. In R. L. Wexelblatt, editor, History of Programming Languages, pages 173–197. Academic Press, New York, 1981.

McCarthy, John, S. R. Russell, D. Edwards, et al. LISP Programmer's Manual. Massachusetts Institute of Technology, A.I. Lab., Cambridge, Massachusetts, November 1959. Handwritten Draft + Machine Typed.

McKinna, James and Robert Pollack. Pure Type Sytems formalized. In M. Bezem and J. F. Groote, editors, Proceedings of the International Conference on Typed Lambda Calculi and Applications, pages 289–305. Springer-Verlag LNCS 664, March 1993.

Meertens, Lambert. Incremental polymorphic type checking in B. In ACM Symposium on Principles of Programming Languages (POPL), Austin, Texas,1983.

Milner, Robin. A theory of type polymorphism in programming. Journal of Computer and System Sciences, 17:348–375, August 1978.

Milner, Robin. A Calculus of Communicating Systems, volume 92 of Lecture Notes in Computer Science. Springer-Verlag, 1980.

Milner, Robin. Communication and Concurrency. Prentice Hall, 1989.

Milner, Robin. The polyadic π-calculus: a tutorial. Technical Report ECS-LFCS-91-180, Laboratory for Foundations of Computer Science, Department of Computer Science, University of Edinburgh, UK, October 1991. Appeared in Proceedings of the International Summer School on Logic and Algebra of Specification, UK, August 1991. Reprinted in Logic and Algebra of Specification, ed. F. L. Bauer, W. Brauer, and H. Schwichtenberg, Springer-Verlag, 1993.

Milner, Robin. Communicating and Mobile Systems: the Pi-Calculus. Cambridge University Press, 1999.

Milner, Robin, Joachim Parrow, and David Walker. A calculus of mobile processes (Parts I and II). Information and Computation, 100:1–77, 1992.

Milner, Robin and Mads Tofte. Co-induction in relational semantics. Theoretical Computer Science, 87:209–220, 1991a.

Milner, Robin and Mads Tofte. Commentary on Standard ML. MIT Press, Cambridge, Massachusetts, 1991b.

Milner, Robin, Mads Tofte, and Robert Harper. The Definition of Standard ML. MIT Press, 1990.

Milner, Robin, Mads Tofte, Robert Harper, and David MacQueen. The Definition of Standard ML (Revised). MIT Press, 1997.

Mitchell, John C. Coercion and type inference (summary). In ACM Symposium on Principles of Programming Languages (POPL), Salt Lake City, Utah, pages 175–185, January 1984a.

Mitchell, John C. Type inference and type containment. In Proc. Int. Symp. on Semantics of Data Types, Sophia-Antipolis (France), pages 257–278, BerlinJune 1984b. Springer LNCS 173. Full version in Information and Computation, vol. 76, no. 2/3, 1988, pp. 211–249. Reprinted in Logical Foundations of Functional Programming, ed. G. Huet, Addison-Wesley (1990) 153–194.

Mitchell, John C. Representation independence and data abstraction (preliminary version). In ACM Symposium on Principles of Programming Languages (POPL), St. Petersburg Beach,Florida, pages 263–276, 1986.

Mitchell, John C. Toward a typed foundation for method specialization and inheritance. In ACM Symposium on Principles of Programming Languages (POPL), San Francisco, California, pages 109–124, January 1990a. Also in Carl A. Gunter and John C. Mitchell, editors, Theoretical Aspects of Object-Oriented Programming: Types, Semantics, and Language Design (MIT Press, 1994).

Mitchell, John C. Type systems for programming languages. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, Volume B, pages 365–458. North-Holland, Amsterdam, 1990b.

Mitchell, John C. Foundations for Programming Languages. MIT Press, Cambridge, Massachusetts, 1996.

Mitchell, John C. and Robert Harper. The essence of ML. In ACM Symposium on Principles of Programming Languages (POPL), San Diego, California, January 1988. Full version in ACM Transactions on Programming Languages and Systems, vol. 15, no. 2, 1993, pp. 211–252, under the title "On the type structure of Standard ML".

Mitchell, John C. and Albert R. Meyer. Second-order logical relations (extended abstract). In Rohit Parikh, editor, Logic of Programs, volume 193 of Lecture Notes in Computer Science, pages 225–236, Berlin, 1985. Springer-Verlag.

Mitchell, John C. and Gordon D. Plotkin. Abstract types have existential types. ACM Trans. on Programming Languages and Systems, 10(3):470–502, 1988. Summary in ACM Symposium on Principles of Programming Languages (POPL), New Orleans, Louisiana, 1985.

Morris, James H. Lambda calculus models of programming languages. Technical Report MIT-LCS//MIT/LCS/TR-57, Massachusetts Institute of Technology, Laboratory for Computer Science, December 1968.

Morrisett, Greg, Matthias Felleisen, and Robert Harper. Abstract models of memory management. In Proceedings of the Seventh International Conference on Functional Programming Languages and Computer Architecture (FPCA'95), pages 66–77, La Jolla, California, June 25–28, 1995. ACM SIGPLAN/SIGARCH and IFIP WG2.8, ACM Press.

Morrisett, Greg, David Walker, Karl Crary, and Neal Glew. From System F to Typed Assembly Language. In ACM Symposium on Principles of Programming Languages (POPL), San Diego, California, pages 85–97, January 1998.

Mugridge, Warwick B., John Hamer, and John G. Hosking. Multi-methods in a statically-typed programming language. In Pierre America, editor, ECOOP '91: European Conference on Object-Oriented Programming, volume 512 of Lecture Notes in Computer Science, pages 307–324. Springer-Verlag, 1991.

Mycroft, Alan. Dynamic types in ML. Manuscript, 1983.

Mycroft, Alan. Polymorphic type schemes and recursive definitions. In M. Paul and B. Robinet, editors, Proceedings of the International Symposium on Programming, volume 167 of LNCS, pages 217–228, Toulouse, France, April 1984. Springer.

Myers, Andrew C., Joseph A. Bank, and Barbara Liskov. Parameterized types for Java. In ACM Symposium on Principles of Programming Languages (POPL), Paris, France, pages 132–145, January 1997.

Nadathur, Gopalan and Dale Miller. An overview of λProlog. In Robert A. Kowalski and Kenneth A. Bowen, editors, Logic Programming: Proceedings of the Fifth International Conference and Symposium, Volume 1, pages 810–827, MIT Press, Cambridge, Massachusetts, August 1988.

Naur, Peter et al. Revised report on the algorithmic language Algol 60. Communications of the ACM, 6:1–17, January 1963.

Necula, George C. Proof-carrying code. In ACM Symposium on Principles of Programming Languages (POPL), Paris, France, pages 106–119, 15–17 January 1997.

Necula, George C. and Peter Lee. Safe kernel extensions without run-time checking. In 2nd Symposium on Operating Systems Design and Implementation (OSDI '96), October 28–31, 1996, Seattle, WA, pages 229–243, Berkeley, CA, USA, October 1996. USENIX press.

Necula, George C. and Peter Lee. Safe, untrusted agents using proof-carrying code. In G. Vigna, editor, Mobile Agents and Security, volume 1419 of Lecture Notes in Computer Science, pages 61–91. Springer-Verlag, 1998.

Nelson, Greg, editor.Systems Programming with Modula-3. Prentice-Hall, 1991.

Nipkow, Tobias and David von Oheimb. Java_light is type-safe — definitely. In ACM Symposium on Principles of Programming Languages (POPL), San Diego, California, pages 161–170, January 1998.

O'Callahan, Robert and Daniel Jackson. Lackwit: A program understanding tool based on type inference. In Proceedings of the 1997 International Conference on Software Engineering, pages 338–348. ACM Press, 1997.

Odersky, Martin. Functional nets. In Proc. European Symposium on Programming (ESOP), pages 1–25. Springer-Verlag, 2000. Lecture Notes in Computer Science 1782.

Odersky, Martin and Konstantin L ufer. Putting type annotations to work. In ACM Symposium on Principles of Programming Languages (POPL), St. Petersburg Beach,Florida, pages 54–67, St. Petersburg Beach, Florida, January 21–24, 1996. ACM Press.

Odersky, Martin, Martin Sulzmann, and Martin Wehr. Type inference with constrained types. Theory and Practice of Object Systems, 5(1):35–55, 1999. Summary in Workshop on Foundations of Object-Oriented Languages (FOOL), informal proceedings, 1997.

Odersky, Martin and Philip Wadler. Pizza into Java: Translating theory into practice. In ACM Symposium on Principles of Programming Languages (POPL), Paris, France, pages 146–159, January 1997.

Odersky, Martin and Christoph Zenger. Nested types. In Workshop on Foundations of Object-Oriented Languages (FOOL 8), January 2001.

Odersky, Martin, Christoph Zenger, and Matthias Zenger. Colored local type inference. ACM SIGPLAN Notices, 36(3):41–53, March 2001.

O'Hearn, Peter W., Makoto Takeyama, A. John Power, and Robert D. Tennent. Syntactic control of interference revisited. In MFPS XI, conference on Mathematical Foundations of Program Semantics, volume 1 of Electronic Notes in Theoretical Computer Science. Elsevier, March 1995.

O'Toole, James W. and David K. Gifford. Type reconstruction with first-class polymorphic values. In ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), Portland, Oregon, pages 207–217, June 1989.

Palsberg, Jens and Christina Pavlopoulou. From polyvariant flow information to intersection and union types. In ACM Symposium on Principles of Programming Languages (POPL), San Diego, California, pages 197–208, 1998.

Palsberg, Jens and Michael I. Schwartzbach. Object-Oriented Type Systems. Wiley, 1994.

Park, David. Concurrency and automata on infinite sequences. In P. Deussen, editor, Proceedings of the 5th GI-Conference on Theoretical Computer Science, volume 104 of Lecture Notes in Computer Science, pages 167–183. Springer-Verlag, Berlin, 1981.

Paulin-Mohring, Christine. Extracting F_ω's programs from proofs in the calculus of constructions. In ACM Symposium on Principles of Programming Languages (POPL), Austin, Texas, pages 89–104, January 1989.

Paulson, Laurence C. ML for the Working Programmer. Cambridge University Press, New York, NY, second edition, 1996.

Perry, Nigel. The Implementation of Practical Functional Programming Languages. PhD thesis, Imperial College, 1990.

Peyton Jones, Simon L. and David R. Lester. Implementing Functional Languages. Prentice Hall, 1992.

Pfenning, Frank. Partial polymorphic type inference and higher-order unification. In ACM Symposium on Lisp and Functional Programming (LFP), Snowbird, Utah, pages 153–163, July 1988. Also available as Ergo Report 88-048, School of Computer Science, Carnegie Mellon University, Pittsburgh.

Pfenning, Frank. Elf: A language for logic definition and verified meta-programming. In Fourth Annual Symposium on Logic in Computer Science, pages 313–322, Pacific Grove, California, June 1989. IEEE Computer Society Press.

Pfenning, Frank. On the undecidability of partial polymorphic type reconstruction. Fundamenta Informaticae, 19(1,2):185–199, 1993a. Preliminary version available as Technical Report CMU-CS-92-105, School of Computer Science, Carnegie Mellon University, January 1992.

Pfenning, Frank. Refinement types for logical frameworks. In Herman Geuvers, editor, Informal Proceedings of the Workshop on Types for Proofs and Programs, pages 285–299, Nijmegen, The Netherlands, May 1993b.

Pfenning, Frank. Elf: A meta-language for deductive systems. In A. Bundy, editor, Proceedings of the 12th International Conference on Automated Deduction, pages 811–815, Nancy, France, June 1994. Springer-Verlag LNAI 814.

Pfenning, Frank. The practice of logical frameworks. In H l ne Kirchner, editor, Proceedings of the Colloquium on Trees in Algebra and Programming, pages 119– 134, Link ping, Sweden, April 1996. Springer-Verlag LNCS 1059. Invited talk.

Pfenning, Frank. Logical frameworks. In Alan Robinson and Andrei Voronkov, editors, Handbook of Automated Reasoning. Elsevier, 1999.

Pfenning, Frank. Computation and Deduction. Cambridge University Press, 2001.

Pfenning, Frank and Peter Lee. Metacircularity in the polymorphic λ-calculus. The-oretical Computer Science, 89(1):137–159, 21 October 1991. Summary in TAP-SOFT '89, Proceedings of the International Joint Conference on Theory and Practice in Software Development, Barcelona, Spain, pages 345–359, Springer-Verlag LNCS 352, March 1989.

Pierce, Benjamin C. Basic Category Theory for Computer Scientists. MIT Press, 1991a.

Pierce, Benjamin C. Programming with Intersection Types and Bounded Polymorphism. PhD thesis, Carnegie Mellon University, December 1991b. Available as School of Computer Science technical report CMU-CS-91-205.

Pierce, Benjamin C. Bounded quantification is undecidable. Information and Computation, 112(1):131–165, July 1994. Also in Carl A. Gunter and John C. Mitchell, editors, Theoretical Aspects of Object-Oriented Programming: Types, Semantics, and Language Design (MIT Press, 1994). Summary in ACM Symposium on Principles of Programming Languages (POPL), Albuquerque, New Mexico.

Pierce, Benjamin C. Even simpler type-theoretic foundations for OOP. Manuscript (circulated electronically), March 1996.

Pierce, Benjamin C. Bounded quantification with bottom. Technical Report 492, Computer Science Department, Indiana University, 1997a.

Pierce, Benjamin C. Intersection types and bounded polymorphism. Mathematical Structures in Computer Science, 7(2):129–193, April 1997b. Summary in Typed Lambda Calculi and Applications, March 1993, pp. 346–360.

Pierce, Benjamin C. and Davide Sangiorgi. Typing and subtyping for mobile processes. In Logic in Computer Science, 1993. Full version in Mathematical Structures in Computer Science , Vol. 6, No. 5, 1996.

Pierce, Benjamin C. and Martin Steffen. Higher-order subtyping. In IFIP Working Conference on Programming Concepts, Methods and Calculi (PROCOMET), 1994. Full version in Theoretical Computer Science, vol. 176, no. 1–2, pp. 235–282, 1997 (corrigendum in TCS vol. 184 (1997), p. 247).

Pierce, Benjamin C. and David N. Turner. Statically typed friendly functions via partially abstract types. Technical Report ECS-LFCS-93-256, University of Edinburgh, LFCS, April 1993. Also available as INRIA-Rocquencourt Rapport de Recherche No. 1899.

Pierce, Benjamin C. and David N. Turner. Simple type-theoretic foundations for object-oriented programming. Journal of Functional Programming, 4(2):207–247, April 1994. Summary in ACM Symposium on Principles of Programming Languages (POPL), Charleston, South Carolina, 1993.

Pierce, Benjamin C. and David N. Turner. Local type argument synthesis with bounded quantification. Technical Report 495, Computer Science Department, Indiana University, January 1997.

Pierce, Benjamin C. and David N. Turner. Local type inference. In ACM Symposium on Principles of Programming Languages (POPL), San Diego, California, 1998. Full version in ACM Transactions on Programming Languages and Systems (TOPLAS), 22(1), January 2000, pp. 1–44.

Pierce, Benjamin C. and David N. Turner. Pict: A programming language based on the pi-calculus. In Gordon Plotkin, Colin Stirling, and Mads Tofte, editors, Proof, Language and Interaction: Essays in Honour of Robin Milner, pages 455–494. MIT Press, 2000.

Pitts, Andrew M. Polymorphism is set theoretic, constructively. In Pitt, Poign , and Rydeheard, editors,Category Theory and Computer Science, Edinburgh, pages 12–39. Springer-Verlag, 1987. LNCS volume 283.

Pitts, Andrew M. Non-trivial power types can't be subtypes of polymorphic types. In Fourth Annual Symposium on Logic in Computer Science, Pacific Grove, California, pages 6–13. IEEE, June 1989.

Pitts, Andrew M. Parametric polymorphism and operational equivalence. Mathematical Structures in Computer Science, 10:321–359, 2000.

Plasmeijer, Marinus J. CLEAN: a programming environment based on term graph rewriting. Theoretical Computer Science, 194(1–2), March 1998.

Plotkin, Gordon. Call-by-name, call-by-value, and the λ-calculus. Theoretical Computer Science, 1:125–159, 1975.

Plotkin, Gordon and Mart n Abadi. A logic for parametric polymorphism. In M. Bezem and J. F. Groote, editors, Typed Lambda Calculi and Applications (TLCA), Utrecht, The Netherlands, number 664 in Lecture Notes in Computer Science, pages 361–375. Springer-Verlag, March 1993.

Plotkin, Gordon, Mart n Abadi, and Luca Cardelli. Subtyping and parametricity. In Proceedings of the Ninth IEEE Symposium on Logic in Computer Science, pages 310–319, 1994.

Plotkin, Gordon D. Lambda-definability and logical relations. Memorandum SAI-RM-4, University of Edinburgh, Edinburgh, Scotland, October 1973.

Plotkin, Gordon D. LCF considered as a programming language. Theoretical Computer Science, 5:223–255, 1977.

Plotkin, Gordon D. Lambda-definability in the full type hierarchy. In Jonathan P. Seldin and J. Roger Hindley, editors, To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, pages 363–373. Academic Press, London, 1980.

Plotkin, Gordon D. A structural approach to operational semantics. Technical Report DAIMI FN-19, Computer Science Department, Aarhus University, Aarhus, Denmark, 1981.

Poll, Erik. Width-subtyping and polymorphic record update. Manuscript, June 1996.

Pollack, Robert. Implicit syntax. Informal Proceedings of First Workshop on Logical Frameworks,Antibes, May 1990.

Pollack, Robert. The Theory of LEGO: A Proof Checker for the Extended Calculus of Constructions. PhD thesis, University of Edinburgh, 1994.

Pottier, Fran ois. Simplifying subtyping constraints. In International Conference on Functional Programming (ICFP), Amsterdam, The Netherlands, 1997.

Pottinger, Garrell. A type assignment for the strongly normalizable λ-terms. In To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus, and Formalism, pages 561–577. Academic Press, New York, 1980.

Quine, Willard V. Quiddities: An Intermittently Philosophical Dictionary. Harvard University Press, Cambridge, MA, 1987.

Ramsey, Frank P. The foundations of mathematics. Proceedings of the London Mathematical Society, Series 2, 25(5):338–384, 1925. Reprinted in (Braithwaite, 1931).

Ranta, Aarne. Type-Theoretical Grammar. Clarendon Press, Oxford, 1995.

Reade, Chris. Elements of Functional Programming. International Computer Science Series.Addison-Wesley, Wokingham, England, 1989.

Reddy, Uday S. Objects as closures: Abstract semantics of object oriented languages. In ACM Symposium on Lisp and Functional Programming (LFP), Snowbird, Utah, pages 289–297, Snowbird, Utah, July 1988.

Relax. Document Description and Processing Languages — Regular Language Description for XML (RELAX) — Part 1: RELAX Core. Technical Report DTR 22250-1, ISO/IEC,October 2000.

R my, Didier. Typechecking records and variants in a natural extension of ML. In ACM Symposium on Principles of Programming Languages (POPL), Austin, Texas, pages 242–249, January 1989. Long version in Carl A. Gunter and John C. Mitchell, editors, Theoretical Aspects of Object-Oriented Programming: Types, Semantics, and Language Design (MIT Press, 1994).

R my, Didier. Alg bres Touffues. Application au Typage Polymorphe des Objets Enregistrements dans les Langages Fonctionnels. PhD thesis, Universit Paris VII, 1990.

R my, Didier. Extending ML type system with a sorted equational theory. Research Report 1766, Institut National de Recherche en Informatique et Automatisme, Rocquencourt, BP 105, 78 153 Le Chesnay Cedex, France, 1992a.

R my, Didier. Projective ML. In ACM Symposium on Lisp and Functional Programming (LFP), pages 66–75, 1992b.

R my, Didier. Typing record concatenation for free. In ACM Symposium on Principles of Programming Languages (POPL), Albuquerque, New Mexico, January 1992. Also in Carl A. Gunter and John C. Mitchell, editors, Theoretical Aspects of Object-Oriented Programming: Types, Semantics, and Language Design (MIT Press, 1994).

R my, Didier. Programming objects with ML-ART: An extension to ML with abstract and record types. In Masami Hagiya and John C. Mitchell, editors, International Symposium on Theoretical Aspects of Computer Software (TACS), pages 321–346, Sendai, Japan, April 1994. Springer-Verlag.

R my, Didier. Des enregistrements aux objets. M moire d'habilitation diriger desrecherches, Universit de Paris 7,1998. In English, except for introductory chapter; includes (R my, 1989) and (R my, 1992b).

R my, Didier and J r me Vouillon. Objective ML: An effective object-oriented extension to ML. Theory And Practice of Object Systems, 4(1):27–50, 1998. Summary in ACM Symposium on Principles of Programming Languages (POPL), Paris, France, 1997.

Reynolds, John. Three approaches to type structure. In Mathematical Foundations of Software Development. Springer-Verlag, 1985. Lecture Notes in Computer Science No. 185.

Reynolds, John C. Towards a theory of type structure. In Proc. Colloque sur la Programmation, pages 408–425, New York, 1974. Springer-Verlag LNCS 19.

Reynolds, John C. User-defined types and procedural data structures as complementary approaches to data abstraction. In Stephen A. Schuman, editor, New Directions in Algorithmic Languages 1975, pages 157–168, Rocquencourt, France, 1975. IFIP Working Group 2.1 on Algol, INRIA. Reprinted in (Gries, 1978, pages 309–317) and (Gunter and |Mitchell, 1994, pages 13–23).

Reynolds, John C. Syntactic control of interference. In ACM Symposium on Principles of Programming Languages (POPL), Tucson, Arizona, pages 39–46, 1978. Reprinted in O'Hearn and Tennent, ALGOL-like Languages, vol. 1, pages 273–286, Birkh user, 1997.

Reynolds, John C. Using category theory to design implicit conversions and generic operators. In N. D. Jones, editor, Proceedings of the Aarhus Workshop on Semantics-Directed Compiler Generation, number 94 in Lecture Notes in Computer Science. Springer-Verlag, January 1980. Also in Carl A. Gunter and John C. Mitchell, editors, Theoretical Aspects of Object-Oriented Programming: Types, Semantics, and Language Design (MIT Press, 1994).

Reynolds, John C. The Craft of Programming. Prentice-Hall International, London, 1981.

Reynolds, John C. Types, abstraction, and parametric polymorphism. In R. E. A. Mason, editor, Information Processing 83, pages 513–523, Amsterdam, 1983. Elsevier Science Publishers B. V. Amsterdam,

Reynolds, John C. Polymorphism is not set-theoretic. In G. Kahn, D. B. MacQueen, and G. D. Plotkin, editors, Semantics of Data Types, volume 173 of Lecture Notes in Computer Science, pages 145–156, Berlin, 1984. Springer-Verlag.

Reynolds, John C. Preliminary design of the programming language Forsythe. Technical Report CMU-CS-88-159, Carnegie Mellon University,June 1988. Reprinted in O'Hearn and Tennent, ALGOL-like Languages, vol. 1, pages 173–233, Birkh user, 1997.

Reynolds, John C. Syntactic control of interference, part 2. Report CMU-CS-89-130, Carnegie Mellon University, April 1989.

Reynolds, John C. Introduction to part II, polymorphic lambda calculus. In G rard Huet, editor, Logical Foundations of Functional Programming, pages 77–86. Addison-Wesley, Reading, Massachusetts, 1990.

Reynolds, John C. The coherence of languages with intersection types. In T. Ito and A. R. Meyer, editors, Theoretical Aspects of Computer Software (Sendai, Japan) number 526 in Lecture Notes in Computer Science, pages 675–700. Springer-Verlag, September 1991.

Reynolds, John C. Normalization and functor categories. In Olivier Danvy and Peter Dybjer, editors, Preliminary Proceedings of the 1998 APPSEM Workshop on Normalization by Evaluation, NBE '98, (Chalmers, Sweden, May 8–9, 1998), number NS-98-1 in BRICS Note Series, Department of Computer Science,University of Aarhus, May 1998a.

Reynolds, John C. Theories of Programming Languages. Cambridge University Press, 1998b.

Reynolds, John C. and Gordon Plotkin. On functors expressible in the polymorphic typed lambda calculus. Information and Computation, 105(1):1–29, 1993. Summary in (Huet, 1990).

Robinson, Edmund and Robert Tennent. Bounded quantification and record-update problems.Message to Types electronic mail list, October 1988.

Robinson, J. Alan. Computational logic: The unification computation. Machine Intelligence, 6:63–72, 1971.

Russell, Bertrand. Letter to Frege,1902. Reprinted (in English) in J. van Heijenort, editor, From Frege to G del: A Source Book in Mathematical Logic, 1879–1931; Harvard University Press, Cambridge, MA, 1967; pages 124–125.

Schaffert, Justin Craig. A formal definition of CLU. Master's thesis, MIT, January 1978. MIT/LCS/TR-193.

Scheifler, Robert William. A denotational semantics of CLU. Master's thesis, MIT, May 1978. MIT/LCS/TR-201.

Schmidt, David A. Denotational Semantics: A Methodology for Language Development. Allyn and Bacon, 1986.

Schmidt, David A. The Structure of Typed Programming Languages. MIT Press, 1994.

Sch nfinkel, Moses. ber die Bausteine der mathematischen Logik. Mathematische Annalen, 92:305–316, 1924. Translated into English and republished as "On the building blocks of mathematical logic" in (van Heijenoort, 1967, pp. 355–366).

Scott, Michael L. Programming Language Pragmatics. Morgan Kaufmann,1999.

Severi, Paula and Erik Poll. Pure type systems with definitions. In Proceedings of Logical Foundations of Computer Science (LFCS), pages 316–328. Springer-Verlag, 1994. LNCS volume 813.

Shalit, Andrew. The Dylan Reference Manual: The Definitive Guide to the New Object-Oriented Dynamic Language. Addison-Wesley, Reading, Mass., 1997.

Shields, Mark. Static Types for Dynamic Documents. PhD thesis, Department of Computer Science, Oregon Graduate Institute, February 2001.

Simmons, Harold. Derivation and Computation : Taking the Curry-Howard Correspondence Seriously. Number 51 in Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 2000.

Smith, Frederick, David Walker, and Greg Morrisett. Alias types. In Gert Smolka, editor, Ninth European Symposium on Programming, volume 1782 of Lecture Notes in Computer Science, pages 366–381. Springer-Verlag, April 2000.

Smith, Jan, Bengt Nordstr m, and Kent Petersson. Programming in Martin-L f's Type Theory. An Introduction. Oxford University Press, 1990.

Solomon, Marvin. Type definitions with parameters. In ACM Symposium on Principles of Programming Languages (POPL), Tucson, Arizona, pages 31–38, January 23–25, 1978.

Sommaruga, Giovanni. History and Philosophy of Constructive Type Theory, volume 290 of Synthese Library. Kluwer Academic Pub., 2000.

Somogyi, Zoltan, Fergus Henderson, and Thomas Conway. The execution algorithm of Mercury, an efficient purely declarative logic programming language. Journal of Logic Programming, 29(1–3):17–64, October–November 1996.

S rensen, Morten Heine and Pawel Urzyczyn. Lectures on the Curry-Howard isomorphism. Technical Report 98/14 (= TOPPS note D-368), DIKU, Copenhagen, 1998.

Statman, Richard. Completeness, invariance and λ-definability. Journal of Symbolic Logic, 47(1):17–26, 1982.

Statman, Richard. Equality between functionals, revisited. In Harvey Friedman's Research on the Foundations of Mathematics, pages 331–338. North-Holland, Amsterdam, 1985a.

Statman, Richard. Logical relations and the typed λ-calculus. Information and Control, 65(2–3):85–97, May–June 1985b.

Steffen, Martin. Polarized Higher-Order Subtyping. PhD thesis, Universit t Erlangen-N rnberg, 1998.

Stone, Christopher A. and Robert Harper. Deciding type equivalence in a language with singleton kinds. In ACM Symposium on Principles of Programming Languages (POPL), Boston, Massachusetts, pages 214–227, January 19–21, 2000.

Strachey, Christopher. Fundamental concepts in programming languages. Lecture Notes, International Summer School in Computer Programming, Copenhagen, August 1967. Reprinted in Higher-Order and Symbolic Computation, 13(1/2), pp. 1–49, 2000.

Stroustrup, Bjarne. The C++ Programming Language. Addison Wesley Longman, Reading, MA, third edition,1997.

Studer, Thomas. Constructive foundations for featherweight java. In R. Kahle, P. Schroeder-Heister, and R. St rk, editors, Proof Theory in Computer Science. Springer-Verlag, 2001. Lecture Notes in Computer Science, volume 2183.

Sumii, Eijiro and Benjamin C. Pierce. Logical relations for encryption. In Computer Security Foundations Workshop, June 2001.

Sussman, Gerald Jay and Guy Lewis Steele, Jr.Scheme: an interpreter for extended lambda calculus. MIT AI Memo 349, Massachusetts Institute of Technology, December 1975. Reprinted, with a foreword, in Higher-Order and Symbolic Computation, 11(4), pp. 405–439, 1998.

Syme, Don. Proving Java type soundness. Technical Report 427, Computer Laboratory, University of Cambridge, June 1997.

Tait, William W. Intensional interpretations of functionals of finite type I. Journal of Symbolic Logic, 32(2):198–212, June 1967.

Tait, William W. A realizability interpretation of the theory of species. In R. Parikh, editor, Logic Colloquium, volume 453 of Lecture Notes in Mathematics, pages 240–251, Boston, 1975. Springer-Verlag.

Talpin, Jean-Pierre and Pierre Jouvelot. The type and effects discipline. In Proc. IEEE Symp. on Logic in Computer Science, pages 162–173, 1992.

Tarditi, David, Greg Morrisett, Perry Cheng, Christopher Stone, Robert Harper, and Peter Lee. TIL : A type-directed optimizing compiler for ML. In ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), Philadephia, Pennsylvania, pages 181–192, May 21–24 1996.

Tarski, Alfred. A lattice-theoretical fixpoint theorem and its applications. Pacific Journal of Mathematics, 5:285–309, 1955.

Tennent, Robert D. Principles of Programming Languages. Prentice-Hall, 1981.

Terlouw, J. Een nadere bewijstheoretische analyse van GSTTs. Manuscript, University of Nijmegen, Netherlands, 1989.

Thatte, Satish R. Quasi-static typing (preliminary report). In ACM Symposium on Principles of Programming Languages (POPL), San Francisco, California, pages 367–381, 1990.

Thompson, Simon. Type Theory and Functional Programming. Addison Wesley, 1991.

Thompson, Simon. Haskell: The Craft of Functional Programming. Addison Wesley, 1999.

Tiuryn, Jerzy. Type inference problems: A survey. In B. Rovan, editor, Mathematical Foundations of Computer Science 1990, Bansk Bystrica, Czechoslovakia, volume 452 of Lecture Notes in Computer Science, pages 105–120. Springer-Verlag, New York, NY, 1990.

Tofte and Birkedal. A region inference algorithm. ACMTOPLAS: ACM Transactions on Programming Languages and Systems, 20, 1998.

Tofte, Mads. Type inference for polymorphic references. Information and Computation, 89(1), November 1990.

Tofte, Mads and Jean-Pierre Talpin. Implementing the call-by-value lambda-calculus using a stack of regions. In ACM Symposium on Principles of Programming Languages (POPL), Portland, Oregon, January 1994.

Tofte, Mads and Jean-Pierre Talpin. Region-based memory management. Information and Computation, 132(2):109–176, 1 February 1997.

Trifonov, Valery and Scott Smith. Subtyping constrained types. In Proceedings of the Third International Static Analysis Symposium, volume 1145 of LNCS, pages 349–365. Springer-Verlag, September 1996.

Turner, David N., Philip Wadler, and Christian Mossin. Once upon a type. In ACM Symposium on Functional Programming Languages and Computer Architecture (FPCA), San Diego, California, 1995.

Turner, Raymond. Constructive Foundations for Functional Languages. McGraw Hill, 1991.

Ullman, JeMrey D. Elements of ML Programming. Prentice-Hall, ML97 edition,1997.

Ungar, David and Randall B. Smith. Self: The power of simplicity. In ACM Symposium on Object Oriented Programming: Systems, Languages, and Applications (OOPSLA), pages 227–241, 1987.

U.S. Dept. of Defense.Reference Manual for the Ada Programming Language. GPO 008-000-00354-8, 1980.

van Benthem, Johan. Language in Action: Categories, Lambdas, and Dynamic Logic. MIT Press, 1995.

van Benthem, Johan F. A. K. and Alice Ter Meulen, editors.Handbook of Logic and Language. MIT Press, 1997.

van Heijenoort, Jan, editor.From Frege to G del. Harvard University Press, Cambridge, Massachusetts, 1967.

van Wijngaarden, Adriaan, B. J. Mailloux, J. E. L. Peck, C. H. A. Koster, M. Sintzoff, C. H. Lindsey, L. G. L. T. Meertens, and R. G. Fisker. Revised report on the algorithmic language ALGOL 68. Acta Informatica, 5(1–3):1–236, 1975.

Vouillon, J r me. Conception et r alisation d'une extension du langage ML avec des objets. PhD thesis, Universit Paris 7, October 2000.

Vouillon, J r me. Combining subsumption and binary methods: An object calculus with views. In ACM Symposium on Principles of Programming Languages (POPL), London, England, 2001.

Wadler, Philip. Theorems for free! In Functional Programming Languages and Computer Architecture, pages 347–359. ACM Press, September 1989. Imperial College, London.

Wadler, Philip. Linear types can change the world. In TC 2 Working Conference on Programming Concepts and Methods (Preprint), pages 546–566, 1990.

Wadler, Philip. Is there a use for linear logic? In Proceedings of ACM Symposium on Partial Evaluation and Semantics-Based Program Manipulation, pages 255–273, 1991.

Wadler, Philip. New languages, old logic. Dr. Dobbs Journal, December 2000.

Wadler, Philip. The Girard-Reynolds isomorphism. In Naoki Kobayashi and Benjamin Pierce, editors, Theoretical Aspects of Computer Software (TACS), Sendai, Japan, Lecture Notes in Computer Science. Springer-Verlag, 2001.

Wadler, Philip and Stephen Blott. How to make ad-hoc polymorphism less ad hoc. In ACM Symposium on Principles of Programming Languages (POPL), Austin, Texas, pages 60–76, 1989.

Wadsworth, Christopher P. Semantics and pragmatics of the lambda-calculus. PhD thesis, Programming Research Group,Oxford University, 1971.

Wand, Mitchell. Finding the source of type errors. 13th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages (POPL), pages 38–43, 1986.

Wand, Mitchell. Complete type inference for simple objects. In Proceedings of the IEEE Symposium on Logic in Computer Science, Ithaca, NY, June 1987.

Wand, Mitchell. Corrigendum: Complete type inference for simple objects. In Proceedings of the IEEE Symposium on Logic in Computer Science, 1988.

Wand, Mitchell. Type inference for objects with instance variables and inheritance. Technical Report NU-CCS-89-2, College of Computer Science, Northeastern University,February 1989a. Also in Carl A. Gunter and John C. Mitchell, editors, Theoretical Aspects of Object-Oriented Programming: Types, Semantics, and Language Design (MIT Press, 1994).

Wand, Mitchell. Type inference for record concatenation and multiple inheritance. In Fourth Annual IEEE Symposium on Logic in Computer Science, pages 92–97, Pacific Grove, CA, June 1989b.

Weis, Pierre, Mar a-Virginia Aponte, Alain Laville, Michel Mauny, and Asc nder Su rez. The CAML reference manual, Version 2.6. Technical report, Projet Formel, INRIA-ENS, 1989.

Wells, Joe B. Typability and type checking in the second-order λ-calculus are equivalent and undecidable. In Proceedings of the Ninth Annual IEEE Symposium on Logic in Computer Science (LICS), pages 176–185, 1994.

Whitehead, Alfred North and Bertrand Russell. Principia Mathematica. Cambridge University Press, Cambridge, 1910. Three volumes (1910; 1912; 1913).

Wickline, Philip, Peter Lee, Frank Pfenning, and Rowan Davies. Modal types as staging specifications for run-time code generation. ACM Computing Surveys, 30(3es), September 1998. Article 8.

Wille, Christoph. Presenting C#. SAMS Publishing, 2000.

Winskel, Glynn. The Formal Semantics of Programming Languages: An Introduction. MIT Press, 1993.

Wirth, Niklaus. The programming language Pascal. Acta Informatica, 1(1):35–63, 1971.

Wright, Andrew K. Typing references by effect inference. In Bernd Krieg-Bruckner, editor, ESOP '92, 4th European Symposium on Programming, Rennes, France, volume 582 of Lecture Notes in Computer Science, pages 473–491. Springer-Verlag, New York, N.Y., 1992.

Wright, Andrew K. Simple imperative polymorphism.Lisp and Symbolic Computation,8(4):343–355, 1995.

Wright, Andrew K. and Matthias Felleisen. A syntactic approach to type soundness. Information and Computation, 115(1):38–94, 15 November 1994.

Xi, Hongwei and Robert Harper. A dependently typed assembly language. In International Conference on Functional Programming (ICFP), Firenze, Italy, 2001.

Xi, Hongwei and Frank Pfenning. Eliminating array bound checking through dependent types. In ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), Montreal, Canada, pages 249–257, 1998.

Xi, Hongwei and Frank Pfenning. Dependent types in practical programming. In ACM Symposium on Principles of Programming Languages (POPL), San Antonio, Texas, ACM SIGPLAN Notices, pages 214–227, 1999.

XML 1998. Extensible markup language (XML™),February 1998. XML 1.0, W3C Recommendation, http://www.w3.org/XML/.

XS 2000. XML Schema Part 0: Primer, W3C Working Draft. http://www.w3.org/TR/xmlschema-0/,2000.

Yelick, Kathy, Luigi Semenzato, Geoff Pike, Carleton Miyamoto, Ben Liblit, Arvind Krishnamurthy, Paul Hilfinger, Susan Graham, David Gay, Phil Colella, and Alex Aiken. Titanium: a high-performance Java dialect. Concurrency: Practice and Experience, 10(11–13):825–836, September 1998. Special Issue: Java for High-performance Network Computing.

Zwanenburg, Jan. Pure type systems with subtyping. In J.-Y. Girard, editor, Typed Lambda Calculus and Applications (TLCA), pages 381–396. Springer-Verlag, 1999. Lecture Notes in Computer Science, volume 1581.

The secret to creativity is knowing how to hide your sources. —Albert Einstein

---