Skip to main content
SpringerLink
Log in

Using, Understanding, and Unraveling the OCaml Language From Practice to Theory and Vice Versa

  • Conference paper
  • First Online:
Applied Semantics (APPSEM 2000)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 2395))

Included in the following conference series:

Abstract

These course notes are addressed to a wide audience of people interested in modern programming languages in general, ML-like languages in particular, or simply in OCaml, whether they are programmers or language designers, beginners or knowledgeable readers —little pre-requiresite is actually assumed.

They provide a formal description of the operational semantics (evaluation) and statics semantics (type checking) of core ML and of several extensions starting from small variations on the core language to end up with the OCaml language —one of the most popular incarnation of ML— including its object-oriented layer.

The tight connection between theory and practice is a constant goal: formal definitions are often accompanied by OCaml programs: an interpreter for the operational semantics and an algorithm for type reconstruction are included. Conversely, some practical programming situations taken from modular or object-oriented programming patterns are considered, compared with one another, and explained in terms of type-checking problems.

Many exercises with different level of difficulties are proposed all along the way, so that the reader can continuously checks his understanding and trains his skills manipulating the new concepts; soon, he will feel invited to select more advanced exercises and pursue the exploration deeper so as to reach a stage where he can be left on his own.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Martín Abadi and Luca Cardelli. A theory of objects. Springer, 1997.

    Google Scholar 

  2. Martin 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.

    Google Scholar 

  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.

    Google Scholar 

  4. Davide Ancona and Elena Zueca. A theory of mixin modules: Basic and derived operators. Mathematical Structures in Computer Science, 8(4):401–446, August 1998.

    Google Scholar 

  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.

    Google Scholar 

  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.

    Google Scholar 

  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.

    Google Scholar 

  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.

    Google Scholar 

  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.

    Google Scholar 

  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.

    Google Scholar 

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

    Article  Google Scholar 

  12. Emmanuel Chailloux, Pascal Manoury, and Bruno Pagano. Développement d’applications avec Objective Caml. O’Reilly, 2000.

    Google Scholar 

  13. Craig Chambers. The Cecil Language: Specification & Rationale. Technical Report 93-03-05, University of Washington, 1993.

    Google Scholar 

  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.

    Google Scholar 

  15. Guy Cousineau and Michel Mauny. Approche fonctionnelle de la programmation. Ediscience, 1995.

    Google Scholar 

  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.

    Google Scholar 

  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.

    Google Scholar 

  18. Dominic Duggan and Constantinos Sourelis. Mixin modules. In International Conference on Functional Programming 96, pages 262–273. ACM Press, 1996.

    Google Scholar 

  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.

    Google Scholar 

  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.

    Google Scholar 

  21. Kathleen Fisher and John Reppy. Extending Moby with inheritance-based subtyping. In Proceedings of the 14th European Conference on Object-Oriented Programming, 2000.

    Google Scholar 

  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.

    Google Scholar 

  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.

    Chapter  Google Scholar 

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

    Google Scholar 

  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.

    Google Scholar 

  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.

    Google Scholar 

  28. F. Henglein. Polymorphic Type Inference and Semi-Unification. PhD thesis, Courant Institute of Mathematical Sciences, New York University., 1989.

    Google Scholar 

  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.

    Google Scholar 

  30. Paul Hudak. The Haskell School of Expression: Learning Functional Programming through Multimedia. Cambridge University Press, 2000.

    Google Scholar 

  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.

    Google Scholar 

  32. Gérard Huet. The zipper. Journal of Functional Programming, 7(5):549–554, 1997.

    Article  MATH  MathSciNet  Google Scholar 

  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.

    Google Scholar 

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

    Google Scholar 

  35. 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.

    Google Scholar 

  36. Simon Peyton Jones and John Hughes. Report on the programming language Haskell 98. Technical report, http://www.haskell.org, 1999.

  37. Gilles Kahn. Natural semantics. In Symposium on Theoretical Aspects of Computer Science, pages 22–39, 1987.

    Google Scholar 

  38. 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.

    Google Scholar 

  39. 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.

    Google Scholar 

  40. Xavier Leroy. Polymorphic typing of an algorithmic language. Research report 1778, INRIA, 1992.

    Google Scholar 

  41. Xavier Leroy. Typage polymorphe d’un langage algorithmique. Thèse de doctorat, Université Paris 7, 1992.

    Google Scholar 

  42. Xavier Leroy. Applicative functors and fully transparent higher-order modules. In ACM Symposium on Principles of Programming Languages, pages 142–153. ACM Press, 1995.

    Google Scholar 

  43. Xavier Leroy. A syntactic theory of type generativity and sharing. Journal of Functional Programming, 6(5):667–698, 1996.

    MATH  MathSciNet  Google Scholar 

  44. Xavier Leroy. A modular module system. Journal of Functional Programming, 10(3):269–303, 2000.

    Article  MATH  Google Scholar 

  45. Xavier Leroy and Michel Mauny. Dynamics in ML. Journal of Functional Programming, 3(4):431–463, 1993.

    Article  Google Scholar 

  46. 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.

    Google Scholar 

  47. Alberto Martelli and Ugo Montanari. An efficient unification algorithm. ACM Transactions on Programming Languages and Systems, 4(2):258–282, 1982.

    Article  MATH  Google Scholar 

  48. Robin Milner and Mads Tofte. Commentary on Standard ML. The MIT Press, 1991.

    Google Scholar 

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

    Google Scholar 

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

    Google Scholar 

  51. 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.

    Google Scholar 

  52. Martin Odersky, Martin Sulzmann, and Martin Wehr. Type inference with constrained types. TAPOS, 5(1), 1999.

    Google Scholar 

  53. 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.

    Google Scholar 

  54. Martin Odersky, Christoph Zenger, and Matthias Zenger. Colored local type inference. In ACM Symposium on Principles of Programming Languages, 2001.

    Google Scholar 

  55. Atsushi Ohori. A polymorphic record calculus and its compilation. ACM Transactions on Programming Languages and Systems, 17(6):844–895, 1996.

    Article  Google Scholar 

  56. Lawrence C. Paulson. ML for the working programmer. Cambridge University Press, 1991.

    Google Scholar 

  57. 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.

    Google Scholar 

  58. 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.

    Google Scholar 

  59. G. D. Plotkin. A Structural Approach to Operational Semantics. Technical Report DAIMI FN-19, University of Aarhus, 1981.

    Google Scholar 

  60. François Pottier. Simplifying subtyping constraints: a theory. To appear in Information & Computation, August 2000.

    Google Scholar 

  61. 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.

    Google Scholar 

  62. 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.

    Google Scholar 

  63. 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.

    Google Scholar 

  64. 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.

    Article  Google Scholar 

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

    Google Scholar 

  66. Jon G. Riecke and Christopher A. Stone. Privacy via subsumption. Theory and Practice of Object Systems, 1999.

    Google Scholar 

  67. Claudio V. Russo. Types for modules. PhD thesis, University of Edinburgh, 1998.

    Google Scholar 

  68. Simon Thompson. Haskell: the craft of functional programming. Addison-Wesley, 1999.

    Google Scholar 

  69. 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.

    Google Scholar 

  70. 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.

    Google Scholar 

  71. 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.

    Google Scholar 

  72. Pierre Weis and Xavier Leroy. Le langage Caml. Dunod, 1999.

    Google Scholar 

  73. 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.

    Article  MATH  MathSciNet  Google Scholar 

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

    Article  MATH  MathSciNet  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. INRIA-Rocquencourt, USA

    Didier Rémy

Authors
  1. Didier Rémy
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Projet Lemme, INRIA Sophia-Antipolis, 2004 Route des Lucioles, BP 93, 06902, Sophia Antipolis Cedex, France

    Gilles Barthe

  2. Department of Computing Science, Chalmers University of Technology, 412 96, Göteborg, Sweden

    Peter Dybjer

  3. Departamento de Matemática, Universidade do Minho, Campus de Gualtar, 4710-057, Braga, Portugal

    Luís Pinto

  4. Departamento de Informática, Universidade do Minho, Campus de Gualtar, 4710-057, Braga, Portugal

    João Saraiva

Rights and permissions

Reprints and permissions

Copyright information

© 2002 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Rémy, D. (2002). Using, Understanding, and Unraveling the OCaml Language From Practice to Theory and Vice Versa . In: Barthe, G., Dybjer, P., Pinto, L., Saraiva, J. (eds) Applied Semantics. APPSEM 2000. Lecture Notes in Computer Science, vol 2395. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45699-6_9

Download citation

  • DOI: https://doi.org/10.1007/3-540-45699-6_9

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-44044-4

  • Online ISBN: 978-3-540-45699-5

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation