Didier RÉMY
56, rue de la Tombe Issoire
F-75 014 Paris
Email: Didier.Remy@inria.fr
Phone: 33 (0)1 4335 3773
Born on April 8th, 1963. French citizen.
Curriculum Vitæ
Rocquencourt, October 2015

Current position

Interests

Design and formalization of programming languages.
In particular:

Education

Research experience

2019 - now
Senior research scientist at INRIA in the project-team Cambium.
2014 - 2018
Deputy scientific director at INRIA in charge of Algorithmics, Programming, Software, and Architecture.
2006 - 2019
Senior research scientist at INRIA in the project-team Gallium.
1998 - 2005
Senior research scientist at INRIA in the project-team Cristal.
1991 - 1998
Research scientist at INRIA in the project-team Cristal.
1990 - 1991
Post-doc at University of Pennsylvania in Carl Gunter and Val Tannen’s group.
1987 - 1990
PhD student at INRIA in the Formel project-team. under Gérard Huet’s supervision.

Administrative responsabilities

Fev 2014 - Dec 2018
Deputy Scientific Director (ADS) at Inria

Teaching Experience

2008 - 2023
Taught Functional programming and type systems to graduate students of the Parisian Master of Research in Computer Science (MPRI).
1998 - 2006
Professor at École Polytechnique: taught Modularity and object-oriented programming, Compilation, and Understanding and programming operating systems to last year students.
1992 - 1998
Associate Professor at École Polytechnique: taught Programming and Algorithms to first year students; Languages and Compilation to second year students.
1996
Taught Object-oriented languages to first-year students of École Normale Supérieure:.
1995 - 1997
Taught Type systems and operational semantics to graduate students of École Normale Supérieure, École Polytechnique, and Universities of Paris 6 and Paris 7.
1993 - 1995
Taught Type systems and operational semantics to graduate level of University of Paris 7.

PhD supervision

Clément Blaudeau
PhD student at the University of Paris depuis octobre 2021
Formalizing and improving OCaml modules.
Ambre Williams
Graduated from the University of Paris in December 2020
Refactoring functional programs with ornaments.
Gabriel Scherer
Graduated from University of Paris 7 in March 2016
Which types have a unique inhabitant? Focusing on pure program equivalence.
Julien Cretin
Thèse de l’université de Paris 7, soutenue en janvier Graduated from University of Paris 7 in January 2014
Erasable coercions: a unified approach to type systems
Benoit Montagu
Graduated from University of Paris 7 in December 2010
Programming with first-class modules in a core language with subtyping, singleton kinds and open existential types
Boris Yakobowski
Graduated from University of Paris 7 in December 2008
Graphical types and constraints: second-order polymorphism and inference.
Daniel Bonniot
Graduated from Écoles des Mines de Paris in November 2005
Modular Typechecking of Multi-Methods.
Alexandre Frey
Graduated from École des Mines de Paris in June 2004
An algebraic approach to typechecking an ML-like language with objects, subtyping, and multi-methods.
Didier Le Botlan
Graduated from École Polytechnique in May 2004
MLF: An extension of ML with second-order polymorphism and explicit instantiation.
Jérôme Vouillon
Graduated from University of Paris 7 in September 2000
Design and implementation of an extension of ML with objets.
François Pottier
Graduated from University of Paris 7 in June 1998
Type inference with subtyping constraints.

PhD Examination

Mickaël Laurent
Committee member for his PhD dissertation, Université Paris Cité (2024)
Cédric Pasteur
Committee member for hisPhD dissertation, École Doctorale Informatique, télécommunications, et électronique de Paris. (2013)
Thomaz Blanc
Committee member for his PhD dissertation, École Polytechnique (2006)
Fabien Dagnat
Reviewer for his PhD dissertation, Institut National Polytechnique de Toulouse (2001)
Maribel Fernandez
Reviewer for her Habilitation dissertation, Univ. de Paris 11 (2000)
Mina Abdiche
Reviewer for her PhD dissertation, Univ. de Paris 11 (2000)
Silvano Dal Zillio
Reviewer for his PhD dissertation, Univ. de Nice-Sophia Antipoli (1999)
Camille Le Moniès de Sagazan
Reviewer for his PhD dissertation, Univ. Paul Sabatier (1995)
Beppe Castagna
Reviewer for his PhD dissertation, Univ. Paris 7 (1994)
Lucky Chillan
Committee member for his PhD dissertation, Univ. Paris 7 (1993)

Journal editing

  1. Member of the editorial board of Journal of Functional Programming 2002–2011.

Program committees

  1. International Symposium on Functional and Logic Programming (FLOPS) Akita, Japan. April 2020.
  2. International Symposium on Functional and Logic Programming (FLOPS) Nagoya, Japan. May 2018.
  3. European Symposium On Programming (ESOP), Eindhoven, The Netherlands. April 2016.
  4. Higher-order, typed, inferred, strict: ACM SIGPLAN ML family workshop, Gothenburg, Sweden. September 2014
  5. Ocaml Users and Developpers workshop, 2012. Co-organisateur, co-président du comité de programme.
  6. International Conference on Functional Programming (ICFP), Baltimore, USA, September 2010.
  7. European Symposium On Programming (ESOP), Paphos, Cyprus, March 2010.
  8. ACM SIGPLAN Workshop on Types in Language Design and Implementation (TLDI), Savannah, Georgia, USA, January 2009.
  9. ACM SIGPLAN Workshop on ML, Victoria, British Columbia, Canada, September 2008.
  10. European Symposium On Programming (ESOP), Vienna, Austria, April 2006.
  11. Foundations and Developments of Object-Oriented Languages (FOOL/WOOD), Charleston USA, January 2006.
  12. Journées Francophones des Langages Applicatifs (JFLA), France, 2005.
  13. Programming Language Design and Implementation (PLDI), Washington DC, USA, June 2004.
  14. European Symposium On Programming (ESOP), France, April 2002.
  15. (Member of the steering committee) ML Family workshop. (2015–2019)
  16. (Member of the steering committee) Ocaml Users and Developpers Workshop (OCaml). (2012–2016)
  17. (Member of the steering committee) International Conference on Functional Programming (ICFP). (1997–2000)
  18. (Member of the steering committee) Foundations of Object Oriented Programming (FOOL). (1998–2001)
  19. (General Chair) International Conference on Functional Programming (ICFP), September 1999.
  20. Principle Of Programming Languages (POPL), San Antonio, Texas, USA, January 1999.
  21. (Program Chair) Workshop on Foundations of Object-Oriented Languages (FOOL), San Diego, USA, January 1998.
  22. Workshop on Foundations of Object-Oriented Languages (FOOL), New Brunswick, USA, July 1996.
  23. International Conference on Functional Programming (ICFP), Philadelphia, USA, May 1996 .
  24. European Symposium On Programming (ESOP), Sweden, April 1996.
  25. Journées Francophones des Langages Applicatifs (JFLA), Montreal, Canada, 1996.
  26. (Program Chair) Workshop on ML and its Applications, Orlando, USA, June 1994.

Software development

  1. Author of WhizzyTEX —an gnu-emacs mode for WYSIWYG incremental previewing LATEX documents while editing.
  2. One of the main contributors to Active-DVI an OCaml DVI previewer.
  3. Indirect contributions to the OCaml implementation, in particular its object-oriented layer, but also its typechecker, and the addition of polymorphic methods, GADTs.
  4. ML-ART: Prototype extension of Caml-Light with extensible records, universal and existential types, and programmable class-based objects.

Other activities

Prices

Publications: Journal articles

[1]
Clément Blaudeau, Didier Rémy, and Gabriel Radanne. Fulfilling OCaml modules with Transparency. Proc. ACM Program. Lang., (OOPSLA’24), 2024. to appear.
[2]
Thomas Williams and Didier Rémy. A Principled Approach to Ornamentation in ML. Proceedings of the ACM on Programming Languages, 2(POPL):21:1–21:30, January 2018.
[3]
Didier Rémy and Boris Yakobowski. A church-style intermediate language for MLF. Theoretical Computer Science, 435(1):77–105, June 2012.
[4]
Didier Le Botlan and Didier Rémy. Recasting MLF. Information and Computation, 207(6):726–785, 2009.
[5]
Jacques Garrigue and Didier Rémy. Extending ML with semi-explicit higher-order polymorphism. Information and Computation, 155(1/2):134–169, 1999. A preliminary version appeared in TACS’97.
[6]
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.
[7]
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. Also appeared as SRC Research Report 120. Preliminary version appeared in the Proceedings of the ACM SigPlan Workshop on ML and its Applications, June 1992.

Publications: Books or book chapters

[8]
François Pottier and Didier Rémy. The essence of ML type inference. In Benjamin C. Pierce, editor, Advanced Topics in Types and Programming Languages, chapter 10, pages 389–489. MIT Press, 2005.
[9]
Didier Rémy. Using, Understanding, and Unraveling the OCaml Language. In Gilles Barthe, editor, Applied Semantics. Advanced Lectures. LNCS 2395., pages 413–537. Springer Verlag, 2002.
[10]
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, 1993.
[11]
Didier Rémy. Typing record concatenation for free. In Carl A. Gunter and John C. Mitchell, editors, Theoretical Aspects Of Object-Oriented Programming. Types, Semantics and Language Design. MIT Press, 1993.

Publications: Conference articles

[12]
Gabriel Scherer and Didier Rémy. Which simple types have a unique inhabitant? In Proceedings of the 20th ACM SIGPLAN International Conference on Functional Programming, ICFP 2015, Vancouver, BC, Canada, September 1-3, 2015, pages 243–255, 2015.
[13]
Gabriel Scherer and Didier Rémy. Full reduction in the face of absurdity. In Programming Languages and Systems - 24th European Symposium on Programming, ESOP 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, London, UK, April 11-18, 2015. Proceedings, pages 685–709, 2015.
[14]
Julien Cretin and Didier Rémy. System F with Coercion Constraints. In Logics In Computer Science (LICS). ACM, July 2014.
[15]
Jacques Garrigue and Didier Rémy. Ambivalent Types for Principal Type Inference with GADTs. In 11th Asian Symposium on Programming Languages and Systems, Melbourne, Australia, December 2013.
[16]
Gabriel Scherer and Didier Rémy. GADTs meet subtyping. In Proceedings of the 22Nd European Conference on Programming Languages and Systems, ESOP’13, pages 554–573, Berlin, Heidelberg, 2013. Springer-Verlag.
[17]
Julien Cretin and Didier Rémy. On the Power of Coercion Abstraction. In Proceedings of the 39th ACM Symposium on Principles of Programming Languages (POPL 2012), Philadephia, PA, USA, January 2012.
[18]
Didier Rémy and Boris Yakobowski. A church-style intermediate language for MLF. In Matthias Blume, Naoki Kobayashi, and German Vidal, editors, Functional and Logic Programming, volume 6009 of Lecture Notes in Computer Science, pages 24–39. Springer Berlin / Heidelberg, 2010.
[19]
Benoît Montagu and Didier Rémy. Modeling abstract types in modules with open existential types. In Proceedings of the 36th ACM Symposium on Principles of Programming Languages (POPL’09), pages 354–365, Savannah, GA, USA, January 2009.
[20]
Didier Rémy and Boris Yakobowski. Efficient Type Inference for the MLF language: a graphical and constraints-based approach. In The 13th ACM SIGPLAN International Conference on Functional Programming (ICFP’08), pages 63–74, Victoria, BC, Canada, September 2008.
[21]
Didier Rémy. Simple, partial type-inference for System F based on type-containment. In Proceedings of the tenth International Conference on Functional Programming, September 2005.
[22]
Roberto Di Cosmo, François Pottier, and Didier Rémy. Subtyping recursive types modulo associative commutative products. In Seventh International Conference on Typed Lambda Calculi and Applications (TLCA’05), Nara, Japan, April 2005.
[23]
Didier Le Botlan and Didier Rémy. MLF: Raising ML to the power of System F. In Proceedings of the Eighth ACM SIGPLAN International Conference on Functional Programming, pages 27–38, August 2003.
[24]
Cédric Fournet, Luc Maranget, Cosimo Laneve, and Didier Rémy. Inheritance in the join calculus. In Foundations of Software Technology and Theoretical Computer Science, volume 1974 of Lecture Notes in Computer Science. Springer, December 2000.
[25]
Didier Rémy. From classes to objects via subtyping. In European Symposium On Programming, volume 1381 of Lecture Notes in Computer Science. Springer, March 1998.
[26]
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.
[27]
Didier Rémy and Jérôme Vouillon. Objective ML: A simple object-oriented extension of ml. In Proceedings of the 24th ACM Conference on Principles of Programming Languages, pages 40–53, Paris, France, January 1997.
[28]
Cédric Fournet, Luc Maranget, Cosimo Laneve, and Didier Rémy. Implicit typing à la ML for the join-calculus. In 8th International Conference on Concurrency Theory (CONCUR’97), volume 1243 of Lecture Notes in Computer Science, pages 196–212, Warsaw, Poland, 1997. Springer.
[29]
Cédric Fournet, Georges Gonthier, Jean-Jacques Lévy, Luc Maranget, and Didier Rémy. A calculus of mobile agents. In 7th International Conference on Concurrency Theory (CONCUR’96), volume 1119 of Lecture Notes in Computer Science, pages 406–421, Pisa, Italy, August 26-29 1996. Springer.
[30]
Carl A. Gunter, Didier Rémy, and Jon G. Riecke. A generalization of exceptions and control in ML. In Proc. ACM Conf. on Functional Programming and Computer Architecture, June 1995.
[31]
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.
[32]
Didier Rémy. Projective ML. In 1992 ACM Conference on Lisp and Functional Programming, pages 66–75, New-York, 1992. ACM press.
[33]
Didier Rémy. Typing record concatenation for free. In Nineteenth Annual Symposium on Principles Of Programming Languages, pages 166–176, 1992.
[34]
Didier Rémy. Records and variants as a natural extension of ML. In Sixteenth Annual Symposium on Principles Of Programming Languages, 1989. See also [10].

Other publications

[35]
Clément Blaudeau, Didier Rémy, and Gabriel Radanne. Retrofitting OCaml modules. In Timothy Bourke and Delphine Demange, editors, JFLA 2023 - 34èmes Journées Francophones des Langages Applicatifs, pages 59–100, Praz-sur-Arly, France, January 2023.
[36]
Steve Kremer, Ludovic Mé, Didier Rémy, and Vincent Roca. Cybersecurity: Current challenges and Inria’s research directions. Number 3 in Inria white book. Inria, January 2019.
[37]
Lucas Baudin and Didier Rémy. Disornamentation. In ML Family Workshop 2018, St. Louis, Missouri, United States, September 2018.
[38]
Didier Rémy. Ornamentation put into Practice in ML. In Seventh Workshop on Mathematically Structured Functional Programming (MSFP 2018), Oxford, United Kingdom, July 2018.
[39]
Didier Rémy. Ornaments: exploiting parametricity for safer, more automated code refactorization and code reuse (invited talk). In Haskell 2017: Proceedings of the 10th ACM SIGPLAN International Symposium on Haskell, pages 1–1, Oxford, United Kingdom, September 2017. ACM Press.
[40]
Thomas Williams and Didier Rémy. A Principled Approach to Ornamentation in ML (extended version). Research report, Inria, November 2017.
[41]
Gabriel Scherer and Didier Rémy. Which simple types have a unique inhabitant? Extended version of [12], 2015.
[42]
Gabriel Scherer and Didier Rémy. Full reduction in the face of absurdity. Research report, INRIA, December 2014.
[43]
Didier Rémy and Julien Cretin. From amber to coercion constraints. In Martin Abadi, Philippa Gardner, Andrew D. Gordon, and Radu Mardare, editors, Essays for the Luca Cardelli Fest, number MSR-TR-2014-104 in TechReport. Microsoft Research, September 2014.
[44]
Thomas Williams, Pierre-Évariste Dagand, and Didier Rémy. Ornaments in practice. September 2014.
[45]
Thomas Williams, Pierre-Évariste Dagand, and Didier Rémy. Ornaments in practice. In WGP+ ’14: Proceedings of the 10th ACM SIGPLAN Workshop on Generic Programming, New York, NY, USA, July 2014. ACM.
[46]
Julien Cretin and Didier Rémy. System F with Coercion Constraints. Rapport de recherche RR-8456, INRIA, January 2014.
[47]
Julien Cretin and Didier Rémy. Coherent coercion abstration with a step-indexed strong-reduction semantics. available at http://gallium.inria.fr/ remy/coercions/, July 2013.
[48]
Jacques Garrigue and Didier Rémy. Tracing ambiguity in GADT type inference. Unpublished, June 2012.
[49]
Julien Cretin and Didier Rémy. Extending System F-eta with Abstraction over Erasable Coercions. Research Report RR-7587, INRIA, July 2011.
[50]
Benoît Montagu and Didier Rémy. Towards a simpler account of modules and generativity: Abstract types have open existential types. January 2008.
[51]
Didier Rémy and Boris Yakobowski. A graphical presentation of MLF types with a linear-time unification algorithm. In Proceedings of the 2007 ACM SIGPLAN International Workshop on Types in Languages Design and Implementation (TLDI’07), pages 27–38, Nice, France, January 2007. ACM Press.
[52]
Didier Le Botlan and Didier Rémy. Recasting MLF. Research Report 6228, INRIA, Rocquencourt, BP 105, 78 153 Le Chesnay Cedex, France, June 2007.
[53]
Didier Rémy and Boris Yakobowski. A graphical presentation of MLF types with a linear-time incremental unification algorithm. Extended version of [51], July 2006.
[54]
François Pottier and Didier Rémy. The essence of ML type inference. Extended preliminary version of [8], 2003.
[55]
Carl A. Gunter, Didier Rémy, and Jon G. Riecke. Return types for functional continuations. A preliminary version appeared as [30], 1998.
[56]
Didier Rémy. Re-exploring multiple inheritance. Invited talk at FOOL’7, January 2000.
[57]
Didier Rémy and Jérôme Vouillon. The reality of virtual types for free! Unpublished note avaliable electronically, October 1998.
[58]
Didier Rémy. Des enregistrements aux objets. Mémoire d’habilitation à diriger des recherches, Université de Paris 7, 1998.
[59]
Didier Rémy. From classes to objects via subtyping. A preliminary version appeared in LNCS 1381 (ESOP 98), June 1998.
[60]
Didier Rémy. A case study of typechecking with constrained types: Typing record concatenation. Presented at the workshop on Advances in types for computer science at the Newton Institute, Cambridge, UK, August 1995.
[61]
Didier Rémy. Better subtypes and row variables for record types. Presented at the workshop on Advances in types for computer science at the Newton Institute, Cambridge, UK, August 1995.
[62]
Benjamin C. Pierce, Didier Rémy, and David N. Turner. A typed higher-order programming language based on the pi-calculus. A preliminary version was presented at the Workshop on Type Theory and its Application to Computer Systems, Kyoto University, July 1993.
[63]
Carl A. Gunter and Didier Rémy. A proof-theoretic assessment of runtime type errors. Research Report 11261-921230-43TM, AT&T Bell Laboratories, 600 Mountain Ave, Murray Hill, NJ 07974-2070, 1993.
[64]
Didier Rémy. Efficient representation of extensible records. In Proceedings of the 1992 workshop on ML and its Applications, page 12, San Francisco, USA, June 1992.
[65]
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.
[66]
Didier Rémy. Type Systems for Programming Languages. Course notes, available electronically, 2015.
[67]
Xavier Leroy and Didier Rémy. Programmation du système Unix en OCaml. Course notes, available electronically, 2008.
[68]
Didier Rémy. Syntactic theories and the algebra of record terms. Research Report 1869, Institut National de Recherche en Informatique et Automatisme, Rocquencourt, BP 105, 78 153 Le Chesnay Cedex, France, 1993.
[69]
Didier Rémy. Type inference for records in a natural extension of ML. Research Report 1431, Institut National de Recherche en Informatique et Automatisme, Rocquencourt, BP 105, 78 153 Le Chesnay Cedex, France, May 1991. See also [10] and [34].
[70]
Didier Rémy. Algèbres Touffues. Application au Typage Polymorphe des Objets Enregistrements dans les Langages Fonctionnels. Thèse de doctorat, Université de Paris 7, 1990.