Previous Up Next

References

[1]
Martín Abadi and Luca Cardelli. A theory of objects. Springer, 1997.
[2]
Martín Abadi, Luca Cardelli, Benjamin C. Pierce, and Didier Rémy. Dynamic typing in polymorphic languages. Journal of Functional Programming, 5(1):111–130, January 1995.
[3]
Alexander Aiken and Edward L. Wimmers. Type inclusion constraints and type inference. In Conference on Functional Programming Languages and Computer Architecture, pages 31–41. ACM press, 1993.
[4]
Davide Ancona and Elena Zucca. A theory of mixin modules: Basic and derived operators. Mathematical Structures in Computer Science, 8(4):401–446, August 1998.
[5]
Davide Ancona and Elena Zucca. A primitive calculus for module systems. In Gopalan Nadathur, editor, PPDP'99 - International Conference on Principles and Practice of Declarative Programming, volume 1702 of Lecture Notes in Computer Science, pages 62–79. Springer-Verlag, 1999.
[6]
Hans P. Barendregt. The Lambda-Calulus. Its Syntax and Semantics, volume 103 of Studies in Logic and The Foundations of Mathematics. North-Holland, 1984.
[7]
Sylvain Boulmé, Thérèse Hardin, and Renaud Rioboo. Modules, objets et calcul formel. In Actes des Journées Francophones des Langages Applicatifs. INRIA, 1999.
[8]
François Bourdoncle and Stephan Merz. Type checking higher-order polymorphic multi-methods. In Proceedings of the 24th ACM Conference on Principles of Programming Languages, pages 302–315, July 1997.
[9]
Kim B. Bruce, 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.
[10]
Kim B. Bruce, Martin Odersky, and Philip Wadler. A statically safe alternative to virtual types. In European Conference on Object-Oriented Programming (ECOOP), Brussels, July 1998.
[11]
Luca Cardelli and Peter Wegner. On understanding types, data abstraction, and polymorphism. Computing surveys, 17(4):471–522, 1985.
[12]
Emmanuel Chailloux, Pascal Manoury, and Bruno Pagano. Développement d'applications avec Objective Caml. O'Reilly, 2000.
[13]
Craig Chambers. The Cecil Language: Specification & Rationale. Technical Report 93-03-05, University of Washington, 1993.
[14]
Dominique Clément, Joëlle Despeyroux, Thierry Despeyroux, and Gilles Kahn. A simple applicative language: Mini-ML. In proceedings of the conference Lisp and Functional Programming, LFP'86. ACM Press, August 1986. Also appears as INRIA Research Report RR-529, May 1986.
[15]
Guy Cousineau and Michel Mauny. Approche fonctionnelle de la programmation. Ediscience, 1995.
[16]
Luis Damas and Robin Milner. Principal type-schemes for functional programs. In ACM Symposium on Principles of Programming Languages, pages 207–212. ACM Press, 1982.
[17]
Catherine Dubois, François Rouaix, and Pierre Weis. Extensional polymorphism. In Proceedings of the 22th ACM Conference on Principles of Programming Languages, January 1995.
[18]
Dominic Duggan and Constantinos Sourelis. Mixin modules. In International Conference on Functional Programming 96, pages 262–273. ACM Press, 1996.
[19]
J. Eifrig, S. Smith, and V. Trifonov. Type inference for recursively constrained types and its application to OOP. In Mathematical Foundations of Programming Semantics, 1995.
[20]
Kathleen Fisher and John Reppy. The design of a class mechanism for Moby. In Proceedings of the ACM SIGPLAN '99 Conference on Programming Languages, design and Implementations, pages 37–49, Atlanta, May 1999. ACM SIGPLAN, acm press.
[21]
Kathleen Fisher and John Reppy. Extending Moby with inheritance-based subtyping. In Proceedings of the 14th European Conference on Object-Oriented Programming, 2000.
[22]
Alexandre Frey and François Bourdoncle. The Jazz home page. Free software available at http://www.cma.ensmp.fr/jazz/index.html.
[23]
Jacques Garrigue. Programming with polymorphic variants. In ML Workshop, September 1998.
[24]
Jacques Garrigue and Didier Rémy. Extending ML with semi-explicit higher-order polymorphism. In International Symposium on Theoretical Aspects of Computer Software, volume 1281 of Lecture Notes in Computer Science, pages 20–46. Springer, September 1997.
[25]
Carl A. Gunter. Semantics of Programming Languages: Structures and Techniques. Foundations of Computing. MIT Press, 1992.
[26]
Thérèse Accart Hardin and Véronique Donzeau-Gouge Viguié. Concepts et outils de programmation — Le style fonctionnel, le style impératif avec CAML et Ada. Interéditions, 1992.
[27]
Robert Harper and Mark Lillibridge. A type-theoretic approach to higher-order modules with sharing. In ACM Symposium on Principles of Programming Languages, pages 123–137. ACM Press, 1994.
[28]
F. Henglein. Polymorphic Type Inference and Semi-Unification. PhD thesis, Courant Institute of Mathematical Sciences, New York University., 1989.
[29]
J. Roger Hindley and Jonathan P. Seldin. Introduction to Combinators and λ-calculus. Volume 1 of London Mathematical Society Student texts. Cambridge University Press, 1986.
[30]
Paul Hudak. The Haskell School of Expression: Learning Functional Programming through Multimedia. Cambridge University Press, 2000.
[31]
Gérard Huet. Résolution d'équations dans les langages d'ordre 1,2,…,ω. Thèse de doctorat d'état, Université Paris 7, 1976.
[32]
Gérard Huet. The zipper. Journal of Functional Programming, 7(5):549–554, 1997.
[33]
Lalita A. Jategaonkar and John C. Mitchell. ML with extended pattern matching and subtypes (preliminary version). In Proceedings of the ACM Conference on Lisp and Functional Programming, pages 198–211, Snowbird, Utah, July 1988.
[34]
Trevor Jim. Principal typings and type inference. PhD thesis, Massachusetts Institute of Technology, 1996.
[35]
Trevor Jim. What are principal typings and what are they good for? In Principles of Programming Languages, pages 42–53, 1996.
[36]
Mark P. Jones. Qualified Types: Theory and Practice. Cambridge University Press, November 1994.
[37]
Mark P. Jones and Simon Peyton Jones. Lightweight extensible records for haskell. In Proceedings of the 1999 Haskell Workshop, number UU-CS-1999-28 in Technical report, 1999.
[38]
Simon Peyton Jones and John Hughes. Report on the programming language Haskell 98. Technical report, http://www.haskell.org, 1999.
[39]
Gilles Kahn. Natural semantics. In Symposium on Theoretical Aspects of Computer Science, pages 22–39, 1987.
[40]
Claude Kirchner and Jean-Pierre Jouannaud. Solving equations in abstract algebras: a rule-based survey of unification. Research Report 561, Université de Paris Sud, Orsay, France, April 1990.
[41]
Konstantin Läufer and Martin Odersky. Polymorphic type inference and abstract data types. ACM Transactions on Programming Languages and Systems, 16(5):1411–1430, September 1994.
[42]
Xavier Leroy. Polymorphic typing of an algorithmic language. Research report 1778, INRIA, 1992.
[43]
Xavier Leroy. Typage polymorphe d'un langage algorithmique. Thèse de doctorat, Université Paris 7, 1992.
[44]
Xavier Leroy. Applicative functors and fully transparent higher-order modules. In ACM Symposium on Principles of Programming Languages, pages 142–153. ACM Press, 1995.
[45]
Xavier Leroy. A syntactic theory of type generativity and sharing. Journal of Functional Programming, 6(5):667–698, 1996.
[46]
Xavier Leroy. A modular module system. Journal of Functional Programming, 10(3):269–303, 2000.
[47]
Xavier Leroy and Michel Mauny. Dynamics in ML. Journal of Functional Programming, 3(4):431–463, 1993.
[48]
David B. MacQueen and Mads Tofte. A semantics for higher-order functors. In D. Sannella, editor, Programming languages and systems – ESOP '94, volume 788 of Lecture Notes in Computer Science, pages 409–423. Springer-Verlag, 1994.
[49]
Alberto Martelli and Ugo Montanari. An efficient unification algorithm. ACM Transactions on Programming Languages and Systems, 4(2):258–282, 1982.
[50]
Robin Milner and Mads Tofte. Commentary on Standard ML. The MIT Press, 1991.
[51]
Robin Milner, Mads Tofte, Robert Harper, and David MacQueen. The definition of Standard ML (revised). The MIT Press, 1997.
[52]
John C. Mitchell. Foundations for Programming Languages. MIT Press, 1996.
[53]
Martin Odersky and Konstantin Läufer. Putting type annotations to work. In Proceedings of the 23th ACM Conference on Principles of Programming Languages, pages 54–67, January 1996.
[54]
Martin Odersky, Martin Sulzmann, and Martin Wehr. Type inference with constrained types. TAPOS, 5(1), 1999.
[55]
Martin Odersky, Philip Wadler, and Martin Wehr. A second look at overloading. In Proc. ACM Conf. on Functional Programming and Computer Architecture, pages 135–146, June 1995.
[56]
Martin Odersky, Christoph Zenger, and Matthias Zenger. Colored local type inference. In ACM Symposium on Principles of Programming Languages, 2001.
[57]
Atsushi Ohori. A polymorphic record calculus and its compilation. ACM Transactions on Programming Languages and Systems, 17(6):844–895, 1996.
[58]
Lawrence C. Paulson. ML for the working programmer. Cambridge University Press, 1991.
[59]
Benjamin C. Pierce. Bounded quantification is undecidable. Information and Computation, 112(1):131–165, July 1994. Also in Carl A. Gunter and John C. Mitchell, editors, Theoretical Aspects of Object-Oriented Programming: Types, Semantics, and Language Design (MIT Press, 1994). Summary in ACM Symposium on Principles of Programming Languages, Albuquerque, New Mexico.
[60]
Benjamin C. Pierce and David N. Turner. Local type inference. In Proceedings of the 25th ACM Conference on Principles of Programming Languages, 1998. Full version available as Indiana University CSCI Technical Report 493.
[61]
G. D. Plotkin. A Structural Approach to Operational Semantics. Technical Report DAIMI FN-19, University of Aarhus, 1981.
[62]
François Pottier. Simplifying subtyping constraints: a theory. To appear in Information & Computation, August 2000.
[63]
Didier Rémy. 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, 1992.
[64]
Didier Rémy. 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, number 789 in Lecture Notes in Computer Science, pages 321–346, Sendai, Japan, April 1994. Springer-Verlag.
[65]
Didier Rémy. Type inference for records in a natural extension of ML. In Carl A. Gunter and John C. Mitchell, editors, Theoretical Aspects Of Object-Oriented Programming. Types, Semantics and Language Design. MIT Press, 1994.
[66]
Didier Rémy and Jérôme Vouillon. Objective ML: An effective object-oriented extension to ML. Theory And Practice of Object Systems, 4(1):27–50, 1998. A preliminary version appeared in the proceedings of the 24th ACM Conference on Principles of Programming Languages, 1997.
[67]
John C. Reynolds. Theories of Programming Languages. Cambridge University Press, 1998.
[68]
Jon G. Riecke and Christopher A. Stone. Privacy via subsumption. Theory and Practice of Object Systems, 1999.
[69]
Claudio V. Russo. Types for modules. PhD thesis, University of Edinburgh, 1998.
[70]
Simon Thompson. Haskell: the craft of functional programming. Addison-Wesley, 1999.
[71]
Jérôme Vouillon. Combining subsumption and binary methods: An object calculus with views. In ACM Symposium on Principles of Programming Languages. ACM Press, 2000.
[72]
Jérôme Vouillon. Conception et réalisation d'une extension du langage ML avec des objets. Thèe de doctorat, Université Paris 7, October 2000.
[73]
Mitchell Wand. Complete type inference for simple objects. In D. Gries, editor, Second Symposium on Logic In Computer Science, pages 207–276, Ithaca, New York, June 1987. IEEE Computer Society Press.
[74]
Pierre Weis and Xavier Leroy. Le langage Caml. Dunod, 1999.
[75]
Joe B. Wells. Typability and type checking in system f are equivalent and undecidable. Annals of Pure and Applied Logic, 98(1–3):111–156, 1999.
[76]
Joe B. Wells. The essence of principal typings. In Proceedings of the 29th International Colloquim on Automata, Languages, and Programming, LNCS. Springer-Verlag, 2002.
[77]
Andrew K. Wright and Matthias Felleisen. A syntactic approach to type soundness. Information and Computation, 115(1):38–94, 1994.

B.4  List of all exercises

 
Chapter 1
  1:  (**) Representing evaluation contexts
  2:  (*) Progress in lambda-calculus
  3:  (*) Printer for acyclic types
  4:  (*) Free type variables for recursive types
  5:  (**) Generalizable variables
  6:  (*) Non typability of fix-point
  7:  (*) Using the fix point combinator
  8:  (**) Type soundness of the fix-point combinator
  9:  (*) Multiple recursive definitions
  10:  (*) Fix-point with recursive types
  11:  (**) Printing recursive types
  12:  (**) Lambda-calculus with recursive types
 
Chapter 2
  13:  (**) Matching Cards
  14:  (***) Type soundness for data-types
  15:  (**) Data-type definitions
  16:  (*) Booleans as datatype definitions
  17:  (***) Pairs as datatype definitions
  18:  (**) Recursion with datatypes
  19:  (*) Mutually recursive definitions of abbreviations
  20:  (**) Recursion with references
  21:  (**) Type soundness of exceptions
  22:  (**) Recursion with exceptions
 
Chapter 3
  23:  (*) Self types
  24:  (**) Backups
  25:  (***) Logarithmic Backups
  26:  (**) Object-oriented strings
  27:  (**) Object types
  28:  (**) Unification for object types
  29:  Project —type inference for objects
  30:  Project —A widget toolkit
 
Chapter 4
  31:  Polynomials with one variable
 
Chapter 5
  32:  Project —A small subset of the FOC library
 
Chapter A
  33:  (*) Unix commands true and false
  34:  (*) Unix command echo
  35:  (**) Unix cat and grep commands
  36:  (**) Unix wc command

Previous Up Next