9512.net
甜梦文库
当前位置:首页 >> >>

Journal of Functional Programming, 1(4)375–416, 1991a. Summary in


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), Austin, Texas, 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.

568

References

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 de?nitions. In Jon Barwise, editor, Handbook 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 Je?rey 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 Schei?er, and Jim Waldo. The Jini speci?cation. Addison-Wesley, Reading, MA, USA, 1999.

References

569

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. Uni?cation theory. In D. M. Gabbay, C. J. Hogger, and J. A. Robinson, editors, Handbook of Logic in Arti?cial 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 Data?ow 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 Ra?aetà. Basic theory of F-bounded quanti?cation. 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.

570

References

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 Nonwellfounded 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 speci?cation 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 ?rst-order calculus with object extension. In European Conference on Object-Oriented Programming (ECOOP), 1998.

References

571

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 de?nitions for inheritance in objectoriented 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.

572

References

Bruce, Kim B. and Giuseppe Longo. A modest model of records, inheritance, and bounded quanti?cation. Information and Computation, 87:196–240, 1990. Also in Carl A. Gunter and John C. Mitchell, editors, Theoretical Aspects of ObjectOriented 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 higherorder 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. SpringerVerlag, 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 Oltho?. Interfaces for stronglytyped 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 Oltho?, and John Mitchell. Fbounded quanti?cation 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 Oltho?. 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.

References

573

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 Fω . 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.

574

References

Cardone, Felice. Relational semantics for recursive types and bounded quanti?cation. 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 Uni?ed Foundation. SpringerVerlag, 1997. Castagna, Giuseppe, Giorgio Ghelli, and Giuseppe Longo. A calculus for overloaded 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: Speci?cation 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.

References

575

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 F∧ 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 Cli?s, 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.

576

References

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 in?nite 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: Con?uence 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.

References

577

Danvy, Olivier. Type-directed partial evaluation. In John Hatcli?, 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. SpringerVerlag. Davey, Brian A. and Hilary A. Priestley. Introduction to Lattices and Order. Cambridge University Press, 1990. Davies, Rowan. A re?nement-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, 1977 pp. 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. Uni?cation 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 Cli?s, New Jersey, second edition, 1996. Available electronically at http://www.scheme.com/tspl2d/.

578

References

Eidor?, 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 lambdacalculus. 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 objectoriented 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.

References

579

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. Re?nement types for ML. In ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), Toronto, Ontario, June 1991. Frege, Gottlob. Begri?schrift, 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 lambdacalculus. 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.

580

References

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. Gi?ord, 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.

References

581

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 simpli?ed account of polymorphic references. Information Processing Letters, 51(4):201–206, August 1994. See also (Harper, 1996). Harper, Robert. A note on: “A simpli?ed 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 de?ning 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 Languages (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.

582

References

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 higherorder 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. Transactions 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.

References

583

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 ?rst attempt. In Proc. Int. Symp. on Semantics of Data Types, Sophia-Antipolis (France), Springer LNCS 173, pages 69–85. SpringerVerlag, 1984. Hopcroft, John E. and Je?rey 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 ?nite type. In Anne Sjerp Troelstra, editor, Metamathematical Investigation of Intuitionistic Arithmetic and Analysis, volume 344 of Lecture Notes in Mathematics, pages 454–461. SpringerVerlag, 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.

584

References

Huet, Gérard. A uni?cation 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. E?ective ?ow analysis for avoiding runtime 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 de?nitions. 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 quali?ed types, 1994a.

References

585

Jones, Mark P. Quali?ed 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 Gi?ord. Algebraic reconstruction of types and e?ects. 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 de?nition. 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 quanti?cation is decidable. In Proceedings of the ACM SIGPLAN Workshop on ML and its Applications, June 1992. Kelsey, Richard, William Clinger, and Jonathan Rees. Revised5 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 Cli?s, second edition, 1988.

586

References

Kfoury, Assaf J., Harry Mairson, Franklyn Turbak, and Joe B. Wells. Relating typability and expressiveness in ?nite-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 ?nite-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 dexptimecomplete. 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 semiuni?cation 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 ?niterank 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 uni?cation. 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 picalculus. 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. E?cient 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.

References

587

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. SpringerVerlag, 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.

588

References

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 Scha?ert, Robert Schei?er, and Alan Snyder. CLU Reference Manual. Springer-Verlag, 1981. Liskov, Barbara, Alan Snyder, Russell Atkinson, and J. Craig Scha?ert. 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.

References

589

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 quanti?ers 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 Speci?cation, Marktoberdorf, August 1991. Reprinted in Logic and Algebra of Speci?cation, 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.

590

References

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 De?nition of Standard ML. MIT Press, 1990. Milner, Robin, Mads Tofte, Robert Harper, and David MacQueen. The De?nition 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, Berlin, June 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. NorthHolland, 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.

References

591

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 de?nitions. 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 — de?nitely. In ACM Symposium on Principles of Programming Languages (POPL), San Diego, California, pages 161–170, January 1998.

592

References

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, 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. Gi?ord. Type reconstruction with ?rst-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 ?ow 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 in?nite 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.

References

593

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 uni?cation. 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 de?nition and veri?ed meta-programming. In Fourth Annual Symposium on Logic in Computer Science, pages 313–322, Paci?c 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. Re?nement 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. Theoretical Computer Science, 89(1):137–159, 21 October 1991. Summary in TAPSOFT ’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 quanti?cation 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.

594

References

Pierce, Benjamin C. Even simpler type-theoretic foundations for OOP. Manuscript (circulated electronically), March 1996. Pierce, Benjamin C. Bounded quanti?cation 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 Ste?en. 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 quanti?cation. 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, Paci?c 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.

References

595

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-de?nability 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-de?nability 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.

596

References

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 Tou?ues. 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 ObjectOriented 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 des recherches, 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 e?ective 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-de?ned 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

References

597

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 SemanticsDirected 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. (North-Holland). 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. SpringerVerlag, 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.

598

References

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 quanti?cation and record-update problems. Message to Types electronic mail list, October 1988. Robinson, J. Alan. Computational logic: The uni?cation 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. Scha?ert, Justin Craig. A formal de?nition of CLU. Master’s thesis, MIT, January 1978. MIT/LCS/TR-193. Schei?er, 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?n?nkel, 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 de?nitions. 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 De?nitive Guide to the New ObjectOriented 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 de?nitions with parameters. In ACM Symposium on Principles of Programming Languages (POPL), Tucson, Arizona, pages 31–38, January 23–25, 1978.

References

599

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 e?cient purely declarative logic programming language. Journal of Logic Programming, 29(1–3):17–64, October–November 1996. S?rensen, Morten Heine and Pawe? Urzyczyn. Lectures on the Curry-Howard isomorphism. Technical Report 98/14 (= TOPPS note D-368), DIKU, Copenhagen, 1998. Statman, Richard. Completeness, invariance and λ-de?nability. 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. Ste?en, Martin. Polarized Higher-Order Subtyping. PhD thesis, Universit?t ErlangenNü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 ?nite 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.

600

References

Talpin, Jean-Pierre and Pierre Jouvelot. The type and e?ects 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 ?xpoint theorem and its applications. Paci?c 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, Je?rey D. Elements of ML Programming. Prentice-Hall, ML97 edition, 1997.

References

601

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. Sintzo?, 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.

602

References

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, Paci?c 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 speci?cations 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 e?ect 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.

References

603

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 (XMLTM ), 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, Geo? Pike, Carleton Miyamoto, Ben Liblit, Arvind Krishnamurthy, Paul Hil?nger, 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 Highperformance 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


赞助商链接

更多相关文章:
更多相关标签:

All rights reserved Powered by 甜梦文库 9512.net

copyright ©right 2010-2021。
甜梦文库内容来自网络,如有侵犯请联系客服。zhit325@126.com|网站地图