publications.bib

@article{Remy-Williams!ornaments@popl2018,
  title = {{A Principled Approach to Ornamentation in ML}},
  author = {Williams, Thomas and R{\'e}my, Didier},
  url = {https://hal.inria.fr/hal-01666104},
  journal = {{Proceedings of the ACM on Programming Languages}},
  publisher = {{ACM}},
  volume = {2},
  number = {{POPL}},
  url = {http://doi.acm.org/10.1145/3158109},
  pages = {21:1--21:30},
  year = {2018},
  month = jan,
  doi = {10.1145/3158109},
  keywords = { ML ;  Refactoring ;  Logical Relations ;  Dependent Types ; Functional programming ; Polymorphism ; Data types and structures ; Semantics ; Software maintenance tools ; Ornaments},
  pdf = {https://hal.inria.fr/hal-01666104/file/ornaments-popl18-final.pdf},
  hal_id = {hal-01666104},
  hal_version = {v1},
  timestamp = {Fri, 05 Jan 2018 12:57:30 +0100},
  biburl = {https://dblp.org/rec/bib/journals/pacmpl/WilliamsR18},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
@techreport{Remy-Williams!ornaments@inria2017,
  title = {{A Principled Approach to Ornamentation in ML}},
  author = {Williams, Thomas and R{\'e}my, Didier},
  url = {https://hal.inria.fr/hal-01628060},
  type = {Research Report},
  institution = {{Inria}},
  year = {2017},
  month = nov,
  doi = {10.1145/nnnnnnn.nnnnnnn},
  keywords = { ML ; Polymorphism ;  Refactoring ; Data types and structures ;  Dependent Types ;  Logical Relations ; Ornaments ; Semantics ; Software maintenance tools},
  pdf = {https://hal.inria.fr/hal-01628060/file/ornaments-long.pdf},
  hal_id = {hal-01628060},
  hal_version = {v1}
}
@unpublished{Remy-Scherer!sing@long2015,
  author = {Gabriel Scherer and Didier R{\'{e}}my},
  title = {Which simple types have a unique inhabitant?},
  year = {2015},
  category = {D},
  pdf = {focusing/Remy-Scherer!sing@long2015.pdf},
  url = {http://gallium.inria.fr/~remy/focusing/},
  note = {Extended version of~\cite{Remy-Scherer!sing@icfp2015}}
}
@inproceedings{Remy-Scherer!sing@icfp2015,
  author = {Gabriel Scherer and Didier R{\'{e}}my},
  title = {Which simple types have a unique inhabitant?},
  booktitle = {Proceedings of the 20th {ACM} {SIGPLAN} International Conference on
               Functional Programming, {ICFP} 2015, Vancouver, BC, Canada, September
               1-3, 2015},
  category = {C},
  url = {http://gallium.inria.fr/~remy/focusing/},
  pdf = {focusing/Remy-Scherer!sing@icfp2015.pdf},
  urlpublisher = {http://doi.acm.org/10.1145/2784731.2784757},
  doi = {10.1145/2784731.2784757},
  pages = {243--255},
  year = {2015},
  url = {http://gallium.inria.fr/~remy/focusing/}
}
@inproceedings{Remy-Scherer!fich@esop2015,
  author = {Gabriel Scherer and Didier R{\'{e}}my},
  title = {Full Reduction in the Face of Absurdity},
  booktitle = {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},
  year = {2015},
  category = {C},
  pdf = {coercions/Remy-Scherer!fich@esop2015.pdf},
  url = {http://gallium.inria.fr/~remy/coercions/},
  urlpublisher = {http://dx.doi.org/10.1007/978-3-662-46669-8_28},
  doi = {10.1007/978-3-662-46669-8_28}
}
@techreport{Remy-Scherer!fich@rr2014,
  title = {{Full reduction in the face of absurdity}},
  author = {Scherer, Gabriel and R{\'e}my, Didier},
  url = {https://hal.inria.fr/hal-01093910},
  type = {Research Report},
  category = {D},
  institution = {{INRIA}},
  year = {2014},
  month = dec,
  pdf = {https://hal.inria.fr/hal-01093910/file/Scherer-Remy%21fich%40rr2014.pdf},
  hal_id = {hal-01093910},
  hal_version = {v1}
}
@incollection{Remy-Cretin:coercion-constraints@luca2014,
  author = {Didier R{\'e}my and Julien Cretin},
  title = {From Amber to Coercion Constraints},
  booktitle = {Essays for the Luca Cardelli Fest},
  publisher = {Microsoft Research},
  year = 2014,
  editor = {Martin Abadi and Philippa Gardner and Andrew D. Gordon and
                  Radu Mardare},
  number = {MSR-TR-2014-104},
  series = {TechReport},
  month = sep,
  category = {D},
  url = {http://research.microsoft.com/pubs/226237/Luca-Cardelli-Fest-MSR-TR-2014-104.pdf},
  pdf = {coercions/Remy-Cretin:coercion-constraints@luca2014.pdf}
}
@unpublished{Williams-Dagand-Remy:ornaments@dwgp2014,
  author = {Thomas Williams and Pierre-{\'E}variste Dagand and Didier
                  R{\'e}my},
  title = {Ornaments in Practice},
  abstract = {Ornaments have been introduced as a way to describe some
                  changes in datatype definitions that preserve their
                  recursive structure, reorganizing, adding, or dropping
                  some pieces of data.  After a new data structure has been
                  described as an ornament of an older one, some functions
                  operating on the bare structure can be partially or
                  sometimes totally lifted into functions operating on the
                  ornamented structure.  We explore the feasibility and the
                  interest of using ornaments in practice by applying these
                  notions in an ML-like programming language.  We propose a
                  concrete syntax for defining ornaments of datatypes and
                  the lifting of bare functions to their ornamented
                  counterparts, describe the lifting process, and present
                  several interesting use cases of ornaments.  },
  pdf = {ornaments/Williams-Dagand-Remy:ornaments@draft2014.pdf},
  year = 2014,
  month = sep,
  category = {D}
}
@inproceedings{Williams-Dagand-Remy:ornaments@wgp2014,
  author = {Thomas Williams and Pierre-{\'E}variste Dagand and Didier Rémy},
  title = {Ornaments in Practice},
  month = jul,
  booktitle = {WGP+ '14: Proceedings of the 10th ACM SIGPLAN Workshop on Generic Programming},
  year = 2014,
  location = {Vienna, Austria, USA},
  publisher = {ACM},
  address = {New York, NY, USA},
  abstract = { Ornaments have been introduced as a way to describe some
                  changes in datatype definitions that preserve their
                  recursive structure, reorganizing, adding, or dropping
                  some pieces of data.  After a new data structure has been
                  described as an ornament of an older one, some functions
                  operating on the bare structure can be partially or
                  sometimes totally lifted into functions operating on the
                  ornamented structure.  We explore the feasibility and the
                  interest of using ornaments in practice by applying these
                  notions in an ML-like programming language.  We propose a
                  concrete syntax for defining ornaments of datatypes and
                  the lifting of bare functions to their ornamented
                  counterparts, describe the lifting process, and present
                  several interesting use cases of ornaments.  },
  pdf = {ornaments/Williams-Dagand-Remy:ornaments@draft2014.pdf},
  category = {D}
}
@inproceedings{Cretin-Remy!fcc@lics2014,
  author = {Cretin, Julien and R{\'e}my, Didier},
  title = {{System {F} with {C}oercion {C}onstraints}},
  booktitle = {{L}ogics {I}n {C}omputer {S}cience {(LICS)}},
  year = 2014,
  month = jul,
  publisher = {ACM},
  abstract = { We present a second-order lambda-calculus with coercion
                  constraints that generalizes a previous extension of
                  System F with parametric coercion abstractions by allowing
                  multiple but simultaneous type and coercion abstractions,
                  as well as recursive coercions and equi-recursive types.
                  This enables a uniform presentation of several type system
                  features that had previously been studied separately: type
                  containment, bounded and instance-bounded polymorphism,
                  which are already encodable with parametric coercion
                  abstraction, and ML-style subtyping constraints.  Our
                  framework allows for a clear separation of language
                  constructs with and without computational content. We also
                  distinguish coherent coercions that are fully erasable
                  from potentially incoherent coercions that suspend the
                  evaluation---and enable the encoding of GADTs.  \par
                  Technically, type coercions that witness subtyping
                  relations between types are replaced by a more expressive
                  notion of typing coercions that witness subsumption
                  relations between typings, e.g. pairs composed of a typing
                  environment and a type. Our calculus is equipped with full
                  reduction that allows reduction under abstractions---but
                  we also introduce a form of weak reduction as reduction
                  cannot proceed under incoherent type abstractions.  Type
                  soundness is proved by adapting the step-indexed semantics
                  technique to full reduction, moving indices inside terms
                  so as to control the reduction steps internally.  },
  category = {C},
  pdf = {coercions/Cretin-Remy!fcc@lics2014.pdf},
  also = {http://gallium.inria.fr/~remy/coercions/}
}
@techreport{Cretin-Remy!fcc@rr2014,
  hal_id = {hal-00934408},
  url = {http://hal.inria.fr/hal-00934408},
  title = {{System F with Coercion Constraints}},
  author = {Cretin, Julien and R{\'e}my, Didier},
  abstract = {{We present a second-order lambda-calculus with coercion
                  constraints that generalizes a previous extension of
                  System F with parametric coercion abstractions by allowing
                  multiple but simultaneous type and coercion abstractions,
                  as well as recursive coercions and equi-recursive
                  types. This allows to present in a uniform way several
                  type system features that had previously been studied
                  separately: type containment, bounded and instance-bounded
                  polymorphism, which are already encodable with parametric
                  coercion abstraction, and ML-style subtyping
                  constraints. Our framework allows for a clear separation
                  of language constructs with and without computational
                  content. We also distinguish coherent coercions that are
                  fully erasable from potentially incoherent coercions that
                  suspend the evaluation---and enable the encoding of
                  GADTs. Technically, type coercions that witness subtyping
                  relations between types are replaced by a more expressive
                  notion of typing coercions that witness subsumption
                  relations between typings, e.g. pairs composed of a typing
                  environment and a type. Our calculus is equipped with a
                  strong notion of reduction that allows reduction under
                  abstractions---but we also introduce a form of weak
                  reduction as reduction cannot proceed under incoherent
                  type abstractions. Type soundness is proved by adapting
                  the step-indexed semantics technique to strong reduction
                  strategies, moving indices inside terms so as to control
                  the reduction steps internally.}},
  language = {Anglais},
  affiliation = {GALLIUM - INRIA Rocquencourt},
  pages = {36},
  type = {Rapport de recherche},
  institution = {INRIA},
  number = {RR-8456},
  year = {2014},
  month = jan,
  category = {D},
  pdf = {http://hal.inria.fr/hal-00934408/PDF/RR-8456.pdf}
}
@inproceedings{Garrigue-Remy:gadts@aplas2013,
  author = {Garrigue, Jacques and R{\'e}my, Didier},
  title = {{A}mbivalent {T}ypes for {P}rincipal {T}ype {I}nference
                  with {GADT}s},
  booktitle = {11th Asian Symposium on Programming Languages and Systems},
  year = 2013,
  address = {Melbourne, Australia},
  month = dec,
  abstract = { GADTs, short for Generalized Algebraic DataTypes, which
                  allow constructors of algebraic datatypes to be
                  non-surjective, have many useful applications. However,
                  pattern matching on GADTsintroduces local type equality
                  assumptions, which are a source of ambiguities that may
                  destroy principal types---and must be resolved by type
                  annotations. We introduce ambivalent types to tighten the
                  definition of ambiguities and better confine them, so that
                  type inference has principal types, remains monotonic, and
                  requires fewer type annotations.  },
  category = {C},
  pdf = {gadts/Garrigue-Remy:gadts@aplas2013.pdf},
  also = {http://gallium.inria.fr/~remy/gadts/}
}
@misc{Cretin-Remy:fmulti@draft2013,
  author = {Cretin, Julien and R{\'e}my, Didier},
  title = {Coherent Coercion Abstration with a step-indexed
                  strong-reduction semantics},
  howpublished = {available at http://gallium.inria.fr/~remy/coercions/},
  month = jul,
  year = {2013},
  abstract = { The usual notion of type coercions that witness subtyping
                  relations between types is generalized to a more
                  expressive notion of typing coercions that witness
                  subsumption relations between typings, e.g..  pairs
                  composed of a typing environment and a type. This is more
                  expressive and allows for a clearer separation of language
                  constructs with and without computational content.  This
                  is illustrated on a second-order calculus of implicit
                  coercions that allows multiple but simultaneous type and
                  coercion abstractions and has recursive coercions and
                  general recursive types. The calculus is equipped with a
                  very liberal notion of reduction. It models a wide range
                  of type features including type containment, bounded and
                  instance-bounded polymorphism, as well as subtyping
                  constraints as used for ML-style type inference with
                  subtyping.  Type soundness is proved by adapting the
                  step-indexed semantics technique to strong reduction
                  strategies, moving indices inside terms so as to control
                  the reduction steps internally.  },
  category = {D},
  pdf = {coercions/Cretin-Remy!fmulti@draft2013.pdf},
  also = {http://gallium.inria.fr/~remy/coercions}
}
@inproceedings{Scherer-Remy/gadt@esop2013,
  author = {Scherer, Gabriel and R{\'e}my, Didier},
  title = {{GADT}s Meet Subtyping},
  booktitle = {Proceedings of the 22Nd European Conference on Programming
                  Languages and Systems},
  series = {ESOP'13},
  year = {2013},
  isbn = {978-3-642-37035-9},
  location = {Rome, Italy},
  pages = {554--573},
  numpages = {20},
  off = {http://dx.doi.org/10.1007/978-3-642-37036-6_30},
  doi = {10.1007/978-3-642-37036-6_30},
  acmid = {2450309},
  publisher = {Springer-Verlag},
  address = {Berlin, Heidelberg},
  category = {C},
  abstract = { While generalized abstract datatypes (GADT) are now
                  considered well-understood, adding them to a language with
                  a notion of subtyping comes with a few surprises. What
                  does it mean for a GADT parameter to be covariant?  % The
                  answer turns out to be quite subtle and involves
                  fine-grained properties of the subtyping relation that
                  raise interesting design questions.  % We allow variance
                  annotations in GADT definitions, study their soundness,
                  and present a sound and complete algorithm to check them.
                  Our work may be applied to real-world ML-like languages
                  with explicit subtyping such as OCaml, or to languages
                  with general subtyping constraints.  },
  also = {http://gallium.inria.fr/~remy/gadts}
}
@unpublished{Garrigue-Remy:gadts@abs2012,
  category = {D},
  author = {Garrigue, Jacques and R{\'e}my, Didier},
  title = {Tracing ambiguity in {GADT} type inference},
  note = {Unpublished},
  month = jun,
  year = 2012,
  pdf = {http://gallium.inria.fr/~remy/gadts/Garrigue-Remy:gadts@abs2012.pdf},
  abstract = { GADTs, short for Generalized Algebraic DataTypes, extend
                  usual algebraic datatypes with a form of dependent typing
                  that has many useful applications, but raises serious
                  issues for type inference. Pattern matching on GADTs
                  introduces type equalities with limited scopes, which are
                  a source of ambiguities that may destroy principal
                  types---and must be resolved by type annotations.  By
                  tracing ambiguities in types, we may tighten the
                  definition of ambiguities and confine them, so as to
                  request fewer type annotations.  Now in use in OCaml 4.00,
                  this solution also lifts some restriction on object types
                  and polymorphic types that appeared in a previous
                  implementation of GADTs in OCaml.  }
}
@inproceedings{Cretin-Remy:coercions@popl2012,
  title = {{O}n the {P}ower of {C}oercion {A}bstraction},
  author = {Cretin, Julien and R{\'e}my, Didier},
  booktitle = {Proceedings of the 39th {ACM} Symposium on Principles of
                  Programming Languages (POPL 2012)},
  year = 2012,
  address = {Philadephia, PA, USA},
  month = jan,
  category = {C},
  abstract = {{E}rasable coercions in {S}ystem {F}-eta, also known as
                  retyping functions, are well-typed eta-expansions of the
                  identity. {T}hey may change the type of terms without
                  changing their behavior and can thus be erased before
                  reduction.  Coercions in {F}-eta can model subtyping of
                  known types and some displacement of quantifiers, but not
                  subtyping assumptions nor certain form of delayed type
                  instantiation. We generalize F-eta by allowing abstraction
                  over retyping functions. We follow a general approach
                  where computing with coercions can be seen as computing in
                  the lambda-calculus but keeping track of which parts of
                  terms are coercions. We obtain a language where coercions
                  do not contribute to the reduction but may block it and
                  are thus not erasable. We recover erasable coercions by
                  choosing a weak reduction strategy and restricting
                  coercion abstraction to value-forms or by restricting
                  abstraction to coercions that are polymorphic in their
                  domain or codomain. The latter variant subsumes {F}-eta,
                  {F}-sub, and {MLF} in a unified framework.},
  off = {http://dl.acm.org/citation.cfm?doid=2103656.2103699},
  also = {http://gallium.inria.fr/~remy/coercions/}
}
@article{Remy-Yakobowski:xmlf@tcs2011,
  author = {R{\'e}my, Didier and Yakobowski, Boris},
  title = {A Church-Style Intermediate Language for {MLF}},
  journal = {Theoretical Computer Science},
  year = 2012,
  volume = 435,
  number = 1,
  pages = {77--105},
  month = jun,
  category = {A},
  off = {http://dx.doi.org/10.1016/j.tcs.2012.02.026},
  pdf = {http://gallium.inria.fr/~remy/mlf/Remy-Yakobowski:xmlf@tcs2011.pdf},
  also = {http://gallium.inria.fr/~remy/mlf/},
  abstract = {MLF is a type system that seamlessly merges ML-style
                  implicit but second-class polymorphism with System-F
                  explicit first-class polymorphism. We present xMLF, a
                  Church-style version of MLF with full type information
                  that can easily be maintained during reduction. All
                  parameters of functions are explicitly typed and both type
                  abstraction and type instantiation are explicit. However,
                  type instantiation in xMLF is more general than type
                  application in System F. We equip xMLF with a small-step
                  reduction semantics that allows reduction in any context
                  and show that this relation is confluent and type
                  preserving. We also show that both subject reduction and
                  progress hold for weak-reduction strategies, including
                  call-by-value with the value-restriction.}
}
@article{LeBotlan-Remy/recasting-mlf,
  author = {Le Botlan, Didier and R{\'{e}}my, Didier},
  title = {Recasting {MLF}},
  journal = {Information and Computation},
  volume = {207},
  number = {6},
  pages = {726--785},
  year = {2009},
  category = {A},
  issn = {0890-5401},
  doi = {10.1016/j.ic.2008.12.006},
  url = {http://dx.doi.org/10.1016/j.ic.2008.12.006},
  off = {http://dx.doi.org/10.1016/j.ic.2008.12.006},
  ps = {http://gallium.inria.fr/~remy/mlf/recasting-mlf-RR.ps.gz},
  pdf = {http://gallium.inria.fr/~remy/mlf/recasting-mlf-RR.pdf},
  also = {http://gallium.inria.fr/~remy/mlf/},
  keywords = {ML},
  keywords = {System F},
  keywords = {Type inference},
  keywords = {Type checking},
  keywords = {Polymorphism},
  keywords = {First-class polymorphism},
  abstract = {The language MLF is a proposal for a new type system that
  supersedes both ML and System F, allows for efficient, predictable, and
  complete type inference for partially annotated terms.  In this work, we
  revisit the definition of MLF, following a more progressive approach and
  focusing on the design-space and expressiveness.  We introduce a
  Curry-style version iMLF of MLF and provide an interpretation of iMLF
  types as instantiation-closed sets of System-F types, from which we derive
  the definition of type instance in iMLF.  We give equivalent syntactic
  definition of the type-instance, presented as a set of inference rules.
  We also show an encoding of iMLF into the closure of Curry-style System F
  by let-expansion.  We derive the Church-style version eMLF by refining
  types of iMLF so as to distinguish between given and inferred
  polymorphism.  We show an embedding of ML in eMLF and a straightforward
  encoding of System F into eMLF.}
}
@incollection{Pottier-Remy/emlti,
  author = {Fran{\c{c}}ois Pottier and Didier R{\'{e}}my},
  title = {The Essence of {ML} Type Inference},
  booktitle = {Advanced Topics in Types and Programming Languages},
  pages = {389--489},
  publisher = {MIT Press},
  year = {2005},
  editor = {Benjamin C. Pierce},
  chapter = {10},
  url = {http://cristal.inria.fr/attapl/},
  category = {B}
}
@incollection{Remy/appsem,
  author = {Didier R{\'{e}}my},
  title = {{U}sing, {U}nderstanding, and {U}nraveling the {OC}aml
                  {L}anguage},
  booktitle = {{A}pplied {S}emantics. Advanced Lectures. LNCS 2395.},
  publisher = {Springer Verlag},
  year = {2002},
  editor = {Gilles Barthe},
  pages = {413--537},
  isbn = {3-540-44044-5},
  category = {B},
  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
                  prerequiresite 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.  },
  ps = {http://gallium.inria.fr/~remy/cours/appsem/ocaml.ps.gz},
  pdf = {http://gallium.inria.fr/~remy/cours/appsem/ocaml.pdf},
  url = {http://gallium.inria.fr/~remy/cours/appsem/}
}
@article{Garrigue-Remy/poly-ml,
  author = {Jacques Garrigue and Didier R{\'e}my},
  title = {Extending {ML} with Semi-Explicit Higher-Order
                  Polymorphism},
  journal = {Information and Computation},
  year = 1999,
  volume = {155},
  number = {1/2},
  pages = {134--169},
  note = {A preliminary version appeared in TACS'97},
  abstract = {We propose a modest conservative extension to ML that
                  allows semi-explicit first-class polymorphism while
                  preserving the essential properties of type inference.  In
                  our proposal, the introduction of polymorphic types is
                  fully explicit, that is, both introduction points and
                  exact polymorphic types are to be specified.  However, the
                  elimination of polymorphic types is semi-implicit: only
                  elimination points are to be specified as polymorphic
                  types themselves are inferred.  This extension is
                  particularly useful in Objective ML where polymorphism
                  replaces subtyping.  },
  url = {http://www.springerlink.com/content/m303472288241339/},
  hidedvi = {http://gallium.inria.fr/~remy/ftp/iandc.dvi.gz},
  hideps = {http://gallium.inria.fr/~remy/ftp/iandc.ps.gz},
  pdf = {http://gallium.inria.fr/~remy/ftp/iandc.pdf},
  category = {A}
}
@article{Remy-Vouillon/tapos,
  author = {Didier R{\'e}my and J{\'e}r{\^o}me Vouillon},
  title = {Objective {ML}: An effective object-oriented extension to
                  {ML}},
  journal = {Theory And Practice of Object Systems},
  year = 1998,
  volume = {4},
  number = {1},
  pages = {27--50},
  note = {A preliminary version appeared in the proceedings of the
                  24th ACM Conference on Principles of Programming
                  Languages, 1997},
  category = {A},
  abstract = { Objective ML is a small practical extension to ML with
                  objects and top level classes.  It is fully compatible
                  with ML; its type system is based on ML polymorphism,
                  record types with polymorphic access, and a better
                  treatment of type abbreviations.  Objective ML allows for
                  most features of object-oriented languages including
                  multiple inheritance, methods returning self and binary
                  methods as well as parametric classes.  This demonstrates
                  that objects can be added to strongly typed languages
                  based on ML polymorphism.  },
  hidedvi = {http://gallium.inria.fr/~remy/ftp/objective-ml!tapos98.dvi.gz},
  hideps = {http://gallium.inria.fr/~remy/ftp/objective-ml!tapos98.ps.gz},
  pdf = {http://gallium.inria.fr/~remy/ftp/objective-ml!tapos98.pdf}
}
@article{Abadi-Cardelli-Pierce-Remy/dynamics,
  author = {Mart{\'\i}n Abadi and Luca Cardelli and Benjamin C. Pierce
                  and Didier R{\'e}my},
  title = {Dynamic typing in polymorphic languages},
  journal = {Journal of Functional Programming},
  year = 1995,
  volume = 5,
  number = 1,
  pages = {111-130},
  month = {January},
  note = {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.},
  category = {A},
  abstract = { There are situations in programming where some dynamic
                  typing is needed, even in the presence of advanced static
                  type systems.  We investigate the interplay of dynamic
                  types with other advanced type constructions, discussing
                  their integration into languages with explicit
                  polymorphism (in the style of system $F$), implicit
                  polymorphism (in the style of ML), abstract data types,
                  and subtyping.  },
  hideps = {http://gallium.inria.fr/~remy/ftp/dynamics.ps.gz},
  pdf = {http://gallium.inria.fr/~remy/ftp/dynamics.pdf}
}
@incollection{Remy/records,
  author = {Didier R{\'e}my},
  title = {Type Inference for Records in a Natural Extension of {ML}},
  booktitle = {Theoretical Aspects Of Object-Oriented Programming.
                  Types, Semantics and Language Design},
  publisher = {MIT Press},
  year = 1993,
  editor = {Carl A. Gunter and John C. Mitchell},
  category = {B},
  abstract = { We describe an extension of ML with records where
                  inheritance is given by ML generic polymorphism.  All
                  common operations on records but concatenation are
                  supported, in particular the free extension of records.
                  Other operations such as renaming of fields are added.
                  The solution relies on an extension of ML, where the
                  language of types is sorted and considered modulo
                  equations, and on a record extension of types.  The
                  solution is simple and modular and the type inference
                  algorithm is efficient in practice.  },
  hidedvi = {http://gallium.inria.fr/~remy/ftp/taoop1.dvi.gz},
  hideps = {http://gallium.inria.fr/~remy/ftp/taoop1.ps.gz},
  pdf = {http://gallium.inria.fr/~remy/ftp/taoop1.pdf}
}
@incollection{Remy/concat,
  author = {Didier R{\'e}my},
  title = {Typing Record Concatenation for Free},
  booktitle = {Theoretical Aspects Of Object-Oriented Programming.
                  Types, Semantics and Language Design},
  publisher = {MIT Press},
  year = 1993,
  editor = {Carl A. Gunter and John C. Mitchell},
  category = {B},
  abstract = { We show that any functional language with record
                  extension possesses record concatenation for free.  We
                  exhibit a translation from the latter into the former.  We
                  obtain a type system for a language with record
                  concatenation by composing the translation with
                  typechecking in a language with record extension.  We
                  apply this method to a version of ML with record extension
                  and obtain an extension of ML with either asymmetric or
                  symmetric concatenation.  The latter extension is simple,
                  flexible and has a very efficient type inference algorithm
                  in practice.  Concatenation together with removal of
                  fields needs one more construct than extension of records.
                  It can be added to the version of ML with record
                  extension.  However, many typed languages with record
                  cannot type such a construct.  The method still applies to
                  them, producing type systems for record concatenation
                  without removal of fields.  Object systems also benefit of
                  the encoding which shows that multiple inheritance does
                  not actually require the concatenation of records but only
                  their extension },
  hidedvi = {http://gallium.inria.fr/~remy/ftp/taoop2.dvi.gz},
  hideps = {http://gallium.inria.fr/~remy/ftp/taoop2.ps.gz},
  pdf = {http://gallium.inria.fr/~remy/ftp/taoop2.pdf}
}
@incollection{Remy-Yakobowski@flops2010:xmlf,
  author = {R{\'e}my, Didier and Yakobowski, Boris},
  affiliation = {INRIA Paris - Rocquencourt},
  title = {A Church-Style Intermediate Language for {MLF}},
  booktitle = {Functional and Logic Programming},
  category = {C},
  series = {Lecture Notes in Computer Science},
  editor = {Blume, Matthias and Kobayashi, Naoki and Vidal, German},
  publisher = {Springer Berlin / Heidelberg},
  pages = {24-39},
  volume = {6009},
  also = {http://gallium.inria.fr/~remy/mlf/},
  pdf = {http://gallium.inria.fr/~remy/mlf/Remy-Yakobowski@flops2010:xmlf.pdf},
  doi = {http://dx.doi.org/10.1007/978-3-642-12251-4_4},
  off = {http://dx.doi.org/10.1007/978-3-642-12251-4_4},
  abstract = {MLF is a type system that seamlessly merges ML-style
                  implicit but second-class polymorphism with System-F
                  explicit first-class polymorphism. We present xMLF, a
                  Church-style version of MLF with full type information
                  that can easily be maintained during reduction. All
                  parameters of functions are explicitly typed and both type
                  abstraction and type instantiation are explicit. However,
                  type instantiation in xMLF is more general than type
                  application in System F. We equip xMLF with a small-step
                  reduction semantics that allows reduction in any context
                  and show that this relation is confluent and type
                  preserving. We also show that both subject reduction and
                  progress hold for weak-reduction strategies, including
                  call-by-value with the value-restriction.},
  year = {2010}
}
@inproceedings{Montagu-Remy@popl09:fzip,
  author = {Beno{\^\i}t Montagu and Didier R{\'e}my},
  title = {Modeling Abstract Types in Modules with Open Existential
                  Types},
  booktitle = {Proceedings of the 36th {ACM} Symposium on Principles of
                  Programming Languages (POPL'09)},
  year = {2009},
  address = {Savannah, GA, USA},
  month = jan,
  isbn = {978-1-60558-379-2},
  pages = {354--365},
  doi = {http://doi.acm.org/10.1145/1480881.1480926},
  also = {http://gallium.inria.fr/~remy/modules/},
  pdf = {http://gallium.inria.fr/~remy/modules/Montagu-Remy@popl09:fzip.pdf},
  category = {C},
  abstract = {We propose Fzip, a calculus of open existential types that
                  is an extension of System F obtained by decomposing the
                  introduction and elimination of existential types into
                  more atomic constructs. Open existential types model
                  modular type abstraction as done in module systems. The
                  static semantics of Fzip adapts standard techniques to
                  deal with linearity of typing contexts, its dynamic
                  semantics is a small-step reduction semantics that
                  performs extrusion of type abstraction as needed during
                  reduction, and the two are related by subject reduction
                  and progress lemmas. Applying the Curry-Howard
                  isomorphism, Fzip can be also read back as a logic with
                  the same expressive power as second-order logic but with
                  more modular ways of assembling partial proofs. We also
                  extend the core calculus to handle the double vision
                  problem as well as type-level and term-level
                  recursion. The resulting language turns out to be a new
                  formalization of (a minor variant of) Dreyer's internal
                  language for recursive and mixin modules.}
}
@inproceedings{Remy-Yakobowski@icfp08:mlf-type-inference,
  author = {Didier R{\'e}my and Boris Yakobowski},
  title = {{E}fficient {T}ype {I}nference for the {MLF} Language: a
                  graphical and constraints-based approach},
  booktitle = {The 13th ACM SIGPLAN International Conference on
                  Functional Programming (ICFP'08)},
  year = 2008,
  address = {Victoria, BC, Canada},
  month = sep,
  also = {http://gallium.inria.fr/~remy/mlf/},
  pdf = {http://gallium.inria.fr/~remy/mlf/Remy-Yakobowski@icfp08:mlf-type-inference.pdf},
  pages = {63--74},
  doi = {http://doi.acm.org/10.1145/1411203.1411216},
  category = {C},
  abstract = { MLF is a type system that seamlessly merges ML-style type
                  inference with System-F polymorphism. We propose a system
                  of graphic (type) constraints that can be used to perform
                  type inference in both ML or MLF. We show that this
                  constraint system is a small extension of the formalism of
                  graphic types, originally introduced to represent MLF
                  types. We give a few semantic preserving transformations
                  on constraints and propose a strategy for applying them to
                  solve constraints. We show that the resulting algorithm
                  has optimal complexity for MLF type inference, and argue
                  that, as for ML, this complexity is linear under
                  reasonable assumptions.  }
}
@inproceedings{Remy/fml-icfp,
  author = {Didier R{\'e}my},
  title = {Simple, partial type-inference for {System F} based on
                  type-containment},
  booktitle = {Proceedings of the tenth International Conference on
                  Functional Programming},
  year = {2005},
  month = sep,
  category = {C},
  also = {http://gallium.inria.fr/~remy/work/fml},
  ps = {http://gallium.inria.fr/~remy/work/fml/fml-icfp.ps.gz},
  pdf = {http://gallium.inria.fr/~remy/work/fml/fml-icfp.pdf},
  abstract = { We explore partial type-inference for System F based on
                  type-containment. We consider both cases of a purely
                  functional semantics and a call-by-value stateful
                  semantics.  To enable type-inference, we require
                  higher-rank polymorphism to be user-specified via type
                  annotations on source terms. We allow implicit predicative
                  type-containment and explicit impredicative
                  type-instantiation.  We obtain a core language that is
                  both as expressive as System F and conservative over
                  ML. Its type system has a simple logical specification and
                  a partial type-reconstruction algorithm that are both very
                  close to the ones for ML.  We then propose a surface
                  language where some annotations may be omitted and rebuilt
                  by some algorithmically defined but logically incomplete
                  elaboration mechanism.  }
}
@inproceedings{dicosmo-pottier-remy-05,
  author = {Roberto {Di Cosmo} and Fran{\c{c}}ois Pottier and Didier
                  R{\'e}my},
  title = {Subtyping Recursive Types modulo Associative Commutative
                  Products},
  ps = {http://gallium.inria.fr/~fpottier/publis/dicosmo-pottier-remy-tlca05.ps.gz},
  pdf = {http://gallium.inria.fr/~fpottier/publis/dicosmo-pottier-remy-tlca05.pdf},
  long = {http://cristal.inria.fr/~fpottier/publis/dicosmo-pottier-remy-tlca05-long.ps.gz},
  longpdf = {http://cristal.inria.fr/~fpottier/publis/dicosmo-pottier-remy-tlca05-long.pdf},
  booktitle = {Seventh International Conference on Typed Lambda Calculi
                  and Applications (TLCA'05)},
  address = {Nara, Japan},
  month = apr,
  year = {2005},
  category = {C},
  abstract = {This work sets the formal bases for building tools that
                  help retrieve classes in object-oriented libraries. In
                  such systems, the user provides a query, formulated as a
                  set of class interfaces. The tool returns classes in the
                  library that can be used to implement the user's request
                  and automatically builds the required glue code. We
                  propose subtyping of recursive types in the presence of
                  associative and commutative products---that is, subtyping
                  modulo a restricted form of type isomorphisms---as a model
                  of the relation that exists between the user's query and
                  the tool's answers. We show that this relation is a
                  composition of the standard subtyping relation with
                  equality up to associativity and commutativity of products
                  and we present an efficient decision algorithm for it. We
                  also provide an automatic way of constructing coercions
                  between related types.}
}
@inproceedings{Lebotlan-Remy/mlf-icfp,
  author = {Le Botlan, Didier and R{\'e}my, Didier},
  title = {{MLF}: Raising {ML} to the power of {System F}},
  booktitle = {Proceedings of the Eighth {ACM SIGPLAN} International
                  Conference on Functional Programming},
  pages = {27--38},
  year = 2003,
  month = aug,
  ps = {http://gallium.inria.fr/~remy/work/mlf/icfp.ps.gz},
  dvi = {http://gallium.inria.fr/~remy/work/mlf/icfp.dvi.gz},
  pdf = {http://gallium.inria.fr/~remy/work/mlf/icfp.pdf},
  http = {http://gallium.inria.fr/~remy/work/mlf/},
  urlpublisher = {http://doi.acm.org/10.1145/944705.944709},
  category = {C},
  abstract = { We propose a type system {MLF} that generalizes {ML} with
                  first-class polymorphism as in System~{F}.  Expressions
                  may contain second-order type annotations.  Every typable
                  expression admits a principal type, which however depends
                  on type annotations.  Principal types capture all other
                  types that can be obtained by implicit type instantiation
                  and they can be inferred.  All expressions of ML are
                  well-typed without any annotations.  All expressionsof
                  System~{F} can be mechanically encoded into {MLF} by
                  dropping all type abstractions and type applications, and
                  injecting types of lambda-abstractions into {MLF} types.
                  Moreover, only parameters of lambda-abstractions that are
                  used polymorphically need to remain annotated.  }
}
@inproceedings{Fournet-Laneve-Maranget-Remy/ojoin,
  author = {C{\'e}dric Fournet and Luc Maranget and Cosimo Laneve and
                  Didier R{\'e}my},
  title = {Inheritance in the Join Calculus},
  booktitle = {Foundations of Software Technology and Theoretical
                  Computer Science},
  year = 2000,
  month = dec,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  volume = {1974},
  ps = {http://gallium.inria.fr/~remy/work/ojoin/ojoin.ps.gz},
  pdf = {http://gallium.inria.fr/~remy/work/ojoin/ojoin.pdf},
  http = {http://gallium.inria.fr/~remy/work/ojoin/},
  category = {C},
  abstract = { We propose an object-oriented calculus with internal
                  concurrency and class-based inheritance that is built upon
                  the join calculus. Method calls, locks, and states are
                  handled in a uniform manner, using labeled
                  messages. Classes are partial message definitions that can
                  be combined and transformed. We design operators for
                  behavioral and synchronization inheritance. We also give a
                  type system that statically enforces basic safety
                  properties. Our model is compatible with the JoCaml
                  implementation of the join calculus.  }
}
@inproceedings{Remy/classes-to-objects/esop,
  author = {Didier R{\'e}my},
  title = {From Classes to Objects via Subtyping},
  booktitle = {European Symposium On Programming},
  year = 1998,
  month = {March},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  volume = 1381,
  category = {C},
  abstract = { We extend the Abadi-Cardelli calculus of primitive
                  objects with object extension. We enrich object types with
                  a more precise, uniform, and flexible type structure.
                  This enables to type object extension under both width and
                  depth subtyping.  Objects may also have extend-only or
                  virtual contra-variant methods and read-only co-variant
                  methods.  The resulting subtyping relation is richer, and
                  types of objects can be weaken progressively from a class
                  level to a more traditional object level along the subtype
                  relationship.  },
  url = {classes-to-objects.html}
}
@inproceedings{Garrigue-Remy/poly-ml/tacs,
  author = {Jacques Garrigue and Didier R{\'e}my},
  title = {Extending {ML} with Semi-Explicit Higher-Order
                  Polymorphism},
  booktitle = {International Symposium on Theoretical Aspects of Computer
                  Software},
  year = 1997,
  month = {September},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  volume = 1281,
  pages = {20--46},
  category = {C},
  abstract = { We propose a modest conservative extension to ML that
                  allows semi-explicit higher-order polymorphism while
                  preserving the essential properties of ML.  In our
                  proposal, the introduction of polymorphic types remains
                  fully explicit, that is, both the introduction and the
                  exact polymorphic type must be specified.  However, the
                  elimination of polymorphic types is now semi-implicit:
                  only the elimination itself must be specified as the
                  polymorphic type is inferred.  This extension is
                  particularly useful in Objective ML that privileges
                  polymorphism to subtyping.  },
  hidedvi = {http://gallium.inria.fr/~remy/ftp/tacs97.dvi.gz},
  hideps = {http://gallium.inria.fr/~remy/ftp/tacs97.ps.gz},
  pdf = {http://gallium.inria.fr/~remy/ftp/tacs97.pdf}
}
@inproceedings{Remy-Vouillon/objective-ml,
  author = {Didier R{\'e}my and J{\'e}r{\^o}me Vouillon},
  title = {{Objective} {ML}: A simple object-oriented extension of
                  ML},
  booktitle = {Proceedings of the 24th ACM Conference on Principles of
                  Programming Languages},
  address = {Paris, France},
  year = 1997,
  pages = {40--53},
  month = {January},
  category = {C},
  abstract = { Objective ML is a small practical extension to ML with
                  objects and toplevel classes.  It is fully compatible with
                  ML; its type system is based on ML polymorphism, record
                  types with polymorphic access, and a better treatment of
                  type abbreviations.  Objective ML allows for most features
                  of object-oriented languages including multiple
                  inheritance, methods returning self and binary methods as
                  well as parametric classes.  This demonstrates that
                  objects can be added to strongly typed languages based on
                  ML polymorphism.  },
  urlpublisher = {http://doi.acm.org/10.1145/263699.263707},
  hidedvi = {http://gallium.inria.fr/~remy/ftp/objective-ml!popl97.dvi.gz},
  hideps = {http://gallium.inria.fr/~remy/ftp/objective-ml!popl97.ps.gz},
  pdf = {http://gallium.inria.fr/~remy/ftp/objective-ml!popl97.pdf}
}
@inproceedings{Fournet-Laneve-Maranget-Remy/typing-join,
  author = {C{\'e}dric Fournet and Luc Maranget and Cosimo Laneve and
                  Didier R{\'e}my},
  title = {Implicit typing {\`a} la {ML} for the join-calculus},
  booktitle = {8th International Conference on Concurrency Theory
                  (CONCUR'97) },
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  volume = 1243,
  pages = {196--212},
  year = 1997,
  address = {Warsaw, Poland},
  category = {C},
  abstract = { We adapt the Damas-Milner typing discipline to the
                  join-calculus.  The main result is a new generalization
                  criterion that extends the polymorphism of ML to
                  join-definitions.  We prove the correctness of our typing
                  rules with regards to a chemical semantics.  We also
                  relate typed extensions of the core join-calculus to
                  functional languages.  },
  hidedvi = {http://gallium.inria.fr/~remy/ftp/typing-join.dvi.gz},
  hideps = {http://gallium.inria.fr/~remy/ftp/typing-join.ps.gz},
  pdf = {http://gallium.inria.fr/~remy/ftp/typing-join.pdf}
}
@inproceedings{Fournet-Gonthier-Levy-Maranget-Remy/mobile-agents,
  author = {C{\'e}dric Fournet and Georges Gonthier and Jean-Jacques
                  L{\'e}vy and Luc Maranget and Didier R{\'e}my},
  title = {A Calculus of Mobile Agents},
  booktitle = {7th International Conference on Concurrency Theory
                  (CONCUR'96) },
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  volume = 1119,
  pages = {406--421},
  year = 1996,
  month = aug # { 26-29},
  address = {Pisa, Italy},
  category = {C},
  abstract = { We introduce a calculus for mobile agents and give its
                  chemical semantics, with a precise definition for
                  migration, failure, and failure detection. Various
                  examples written in our calculus illustrate how to express
                  remote executions, dynamic loading of remote resources and
                  protocols with mobile agents. We give the encoding of our
                  distributed calculus into the join-calculus. (BibTeX
                  reference.)  },
  hideps = {http://gallium.inria.fr/~remy/ftp/mobile-agents.ps.gz},
  pdf = {http://gallium.inria.fr/~remy/ftp/mobile-agents.pdf}
}
@inproceedings{Gunter-Remy-Riecke/control,
  author = {Carl A. Gunter and Didier R{\'e}my and Jon G. Riecke},
  title = {A Generalization of Exceptions and Control in {ML}},
  booktitle = {Proc. {ACM} Conf. on Functional Programming and Computer
                  Architecture},
  year = 1995,
  month = {June},
  category = {C},
  abstract = { We add functional continuations and prompts to a language
                  with an ML-style type system.  The operators significantly
                  extend and simplify the control operators in SML/NJ, and
                  can be themselves used to implement (simple) exceptions.
                  We prove that well-typed terms never produce run-time type
                  errors and give a module for implementing them in the
                  latest version of SML/NJ.  },
  hidedvi = {http://gallium.inria.fr/~remy/ftp/prompt.dvi.gz},
  hideps = {http://gallium.inria.fr/~remy/ftp/prompt.ps.gz},
  pdf = {http://gallium.inria.fr/~remy/ftp/prompt.pdf},
  http = {http://gallium.inria.fr/~remy/work/cupto/}
}
@inproceedings{Remy/mlart,
  author = {Didier R{\'e}my},
  title = {Programming Objects with {ML-ART}: An extension to {ML}
                  with Abstract and Record Types},
  booktitle = {International Symposium on Theoretical Aspects of Computer
                  Software},
  year = 1994,
  editor = {Masami Hagiya and John C. Mitchell},
  series = {Lecture Notes in Computer Science},
  number = 789,
  pages = {321--346},
  publisher = {Springer-Verlag},
  address = {Sendai, Japan},
  month = {April},
  category = {C},
  abstract = { Class-based objects can be programmed directly and
                  efficiently in a simple extension to ML.  The
                  representation of objects, based on abstract and record
                  types, allows all usual operations such as multiple
                  inheritance, object returning capability, and message
                  transmission to themselves as well as to their super
                  classes.  There is, however, no implicit coercion from
                  objects to corresponding ones of super-classes.  A simpler
                  representation of objects without recursion on values is
                  also described.  The underlying language extends ML with
                  recursive types, existential and universal types, and
                  mutable extensible records.  The language ML-ART is given
                  with a call-by-value semantics for which type soundness is
                  proved.  },
  hidedvi = {http://gallium.inria.fr/~remy/ftp/tacs94.dvi.gz},
  urlpublisher = {http://www.springerlink.com/index/p7136401k626j726.pdf},
  hideps = {http://gallium.inria.fr/~remy/ftp/tacs94.ps.gz},
  pdf = {http://gallium.inria.fr/~remy/ftp/tacs94.pdf}
}
@inproceedings{Remy/projective-ml,
  author = {Didier R{\'e}my},
  title = {Projective {ML}},
  booktitle = {1992 ACM Conference on Lisp and Functional Programming},
  publisher = {{ACM} press},
  address = {New-York},
  pages = {66--75},
  year = 1992,
  category = {C},
  abstract = { In the last five years there have been many proposals for
                  adding records in strongly typed functional languages.  It
                  is agreed that powerful operations should be provided.
                  However the operations are numerous, and there is no
                  agreement yet on which ones are really needed, and what
                  they should do.  Moreover, there is no basic calculus in
                  which these operations can be described very easily.  We
                  propose a projective lambda calculus as the basis for
                  operations on records.  Projections operate on elevations,
                  that is, records with defaults.  This calculus extends
                  lambda calculus while keeping its essential properties.
                  We build projective ML from this calculus by adding the ML
                  Let typing rule to the simply typed projective calculus.
                  We show that projective ML possesses the subject reduction
                  property, which means that well-typed programs can be
                  reduced safely.  Elevations are practical data structures
                  that can be compiled efficiently.  Moreover, standard
                  records are definable in terms of projections.  },
  hidedvi = {http://gallium.inria.fr/~remy/ftp/lfp92.dvi.gz},
  hideps = {http://gallium.inria.fr/~remy/ftp/lfp92.ps.gz},
  pdf = {http://gallium.inria.fr/~remy/ftp/lfp92.pdf}
}
@inproceedings{Remy/free-concatenation,
  author = {Didier R{\'e}my},
  title = {Typing Record Concatenation for Free},
  booktitle = {Nineteenth Annual Symposium on Principles Of Programming
                  Languages},
  pages = {166--176},
  year = 1992,
  hidedvi = {http://gallium.inria.fr/~remy/ftp/free-concatenation.dvi.gz},
  hideps = {http://gallium.inria.fr/~remy/ftp/free-concatenation.ps.gz},
  pdf = {http://gallium.inria.fr/~remy/ftp/free-concatenation.pdf},
  category = {C}
}
@inproceedings{Remy/popl89,
  author = {Didier R{\'e}my},
  title = {Records and Variants as a natural Extension of {ML}},
  booktitle = {Sixteenth Annual Symposium on Principles Of Programming
                  Languages},
  year = 1989,
  note = {See also \cite{Remy/records}.},
  src = {http://doi.acm.org/10.1145/75277.75284},
  category = {C}
}
@techreport{Cretin-Remy:coercions@inria2011,
  category = {D},
  hal_id = {inria-00582570},
  off = {http://hal.inria.fr/inria-00582570/en/},
  title = {{E}xtending {S}ystem {F}-eta with {A}bstraction over
                  {E}rasable {C}oercions},
  author = {Cretin, Julien and R{\'e}my, Didier},
  abstract = {{E}rasable coercions in {S}ystem {F}-eta, also known as
                  retyping functions, are well-typed eta-expansions of the
                  identity. {T}hey may change the type of terms without
                  changing their behavior and can thus be erased before
                  reduction.  Coercions in {F}-eta can model subtyping of
                  known types and some displacement of quantifiers, but not
                  subtyping assumptions nor certain form of delayed type
                  instantiation. We generalize F-eta by allowing abstraction
                  over retyping functions. We follow a general approach
                  where computing with coercions can be seen as computing in
                  the lambda-calculus but keeping track of which parts of
                  terms are coercions. We obtain a language where coercions
                  do not contribute to the reduction but may block it and
                  are thus not erasable. We recover erasable coercions by
                  choosing a weak reduction strategy and restricting
                  coercion abstraction to value-forms or by restricting
                  abstraction to coercions that are polymorphic in their
                  domain or codomain. The latter variant subsumes {F}-eta,
                  {F}-sub, and {MLF} in a unified framework.},
  language = {{E}nglish},
  affiliation = {{GALLIUM} - {INRIA} {R}ocquencourt - {INRIA} },
  pages = {64},
  type = {{R}esearch {R}eport},
  institution = {INRIA},
  number = {{RR}-7587},
  month = jul,
  year = {2011},
  also = {http://gallium.inria.fr/~remy/coercions/},
  pdf = {http://hal.inria.fr/inria-00582570}
}
@unpublished{Montagu-Remy/Fzip,
  author = {Beno{\^\i}t Montagu and Didier R{\'e}my},
  title = {Towards a Simpler Account of Modules and Generativity:
                  Abstract Types have Open Existential Types},
  year = {2008},
  month = jan,
  pdf = {http://gallium.inria.fr/~remy/modules/fzip.pdf},
  also = {http://gallium.inria.fr/~remy/modules/},
  category = {D},
  abstract = { We present a variant of the explicitly-typed second-order
                  polymorphic lambda-calculus with primitive open
                  existential types, i.e. a collection of more atomic
                  constructs for introduction and elimination of existential
                  types. We equip the language with a call-by-value
                  small-step reduction semantics that enjoys the subject
                  reduction property.  Traditional closed existential types
                  can be defined as syntactic sugar. Conversely, programs
                  with no free existential types can be rearranged to only
                  use closed existential types, but the translation is not
                  compositional.We argue that open existential types model
                  abstract types and modules with generativity.  We also
                  introduce a new notion of paths at the level of types
                  instead of terms that allows for writing type annotations
                  more concisely and modularly.  }
}
@inproceedings{Remy-Yakobowski/mlf-graphic-types,
  author = {Didier R{\'e}my and Boris Yakobowski},
  title = {A graphical presentation of {MLF} types with a linear-time
                  unification algorithm},
  booktitle = {Proceedings of the 2007 ACM SIGPLAN International Workshop
                  on Types in Languages Design and Implementation (TLDI'07)},
  year = 2007,
  isbn = {1-59593-393-X},
  pages = {27--38},
  address = {Nice, France},
  month = jan,
  url-publisher = {http://doi.acm.org/10.1145/1190315.1190321},
  publisher = {ACM Press},
  url = {http://gallium.inria.fr/~remy/work/mlf/},
  category = {D},
  abstract = {MLF is a language that extends ML and System F and
                  combines the benefits of both. We propose a dag
                  representation of MLF types that superposes a term-dag,
                  encoding the underlying term-structure with sharing, and a
                  binding tree encoding the binding-structure. Compared to
                  the original definition, this representation is more
                  canonical as it factors out most of the notational
                  details; it is also closely related to first-order
                  terms. Moreover, it permits a simpler and more direct
                  definition of type instance that combines type instance on
                  first-order term-dags, simple operations on dags, and a
                  control that allows or rejects potential instances. Using
                  this representation, we build a linear-time unification
                  algorithm for MLF types, which we prove sound and complete
                  with respect to the specification.}
}
@techreport{Lebotlan-Remy/recasting-mlf-RR,
  author = {Le Botlan, Didier and R{\'{e}}my, Didier},
  title = {Recasting {MLF}},
  year = {2007},
  month = jun,
  institution = {INRIA},
  number = {6228},
  type = {Research Report},
  pages = {60 p.},
  address = {Rocquencourt, BP 105, 78 153 Le Chesnay Cedex, France},
  off = {https://hal.inria.fr/inria-00156628},
  pdf = {http://gallium.inria.fr/~remy/work/mlf/recasting-mlf-RR.pdf},
  also = {http://gallium.inria.fr/~remy/work/mlf/},
  category = {D},
  abstract = {The language MLF has been proposed as an alternative to
                  System F that permits partial type inference a la ML.  It
                  differs from System F by its types and type-instance
                  relation. Unfortunately, the definition of type instance
                  is only syntactic, and not underpined by some underlying
                  semantics. It has so far only been justified a posteriori
                  by the type soundness result.  In this work, we revisit
                  MLF following a more progressive approach stepping on
                  System F.  We argue that System F is not a well-suited
                  language for ML-style type inference because it fails to
                  factorize some closely related typing derivations. We
                  solve this problem in Curry's style MLF by enriching types
                  with a new form of quantification that may represent a
                  whole collection of System F types.  This permits a
                  natural interpretation of MLF types as sets of System-F
                  types and pulling back the instance relation from set
                  inclusion on the interpretations. We also give an
                  equivalent syntactic definition of the type-instance,
                  presented as a set of inference rules.  We derive a
                  Church's style version of MLF by further refining types so
                  as to distinguish between user-provided and inferred type
                  information.  The resulting language is more canonical
                  than the one originally proposed. We show an embedding of
                  ML in MLF and an encoding of System F into MLF.  Besides,
                  as MLF is more expressive than System F, an encoding of
                  MLF is given towards an extension of System F with local
                  binders.}
}
@unpublished{Remy-Yakobowski/mlf-graphic-types/long,
  author = {Didier R{\'e}my and Boris Yakobowski},
  title = {A graphical presentation of {MLF} types with a linear-time
                  incremental unification algorithm.},
  ps = {http://gallium.inria.fr/~remy/work/mlf/mlf-graphic-types.ps.gz},
  pdf = {http://gallium.inria.fr/~remy/work/mlf/mlf-graphic-types.pdf},
  note = {Extended version of
                  \cite{Remy-Yakobowski/mlf-graphic-types}},
  year = 2006,
  month = jul,
  also = {http://gallium.inria.fr/~remy/work/mlf/},
  category = {D},
  abstract = { MLF is a language that extends both ML and System F and
                  combines the benefits of both. We propose a dag
                  representation of MLF types that superposes a term-dag,
                  encoding the underlying term-structure with sharing, and a
                  binding tree, encoding the binding-structure. This
                  representation is more canonical as it factors out most of
                  the notational details of the original definition; it is
                  also closely related to first-order terms. Moreover, it
                  permits a simpler and more direct definition of type
                  instance that combines type-instance on first-order
                  term-dags, simple operations on dags, and a control that
                  allows or rejects potential instances. Thanks to this
                  representation, we obtain an incremental linear-time
                  unification algorithm for MLF types, which we prove sound
                  and complete with respect to the specification.  We also
                  extend term graphs to express constraints on graphs that
                  can be rewritten incrementally, which suffices to describe
                  all operations needed by type inference.  }
}
@unpublished{Pottier-Remy/emlti-preversion,
  author = {Fran{\c{c}}ois Pottier and Didier R{\'e}my},
  title = {The Essence of {ML} Type Inference},
  year = {2003},
  note = {Extended preliminary version of \cite{Pottier-Remy/emlti}},
  ps = {http://cristal.inria.fr/attapl/preversion.ps.gz},
  also = {http://cristal.inria.fr/attapl/},
  category = {D}
}
@unpublished{Gunter-Remy-Riecke/control-extended,
  author = {Carl A. Gunter and Didier R{\'e}my and Jon G. Riecke},
  title = {Return types for Functional Continuations},
  note = {A preliminary version appeared as
                  \cite{Gunter-Remy-Riecke/control}},
  year = {1998},
  category = {D},
  abstract = { We add functional continuations and prompts to a language
                  with an ML-style type system.  The operators significantly
                  extend and simplify the control operators in SML/NJ, and
                  can be themselves used to implement (simple) exceptions.
                  We prove that well-typed terms never produce run-time type
                  errors and give a module for implementing them in the
                  latest version of SML/NJ.  },
  hidedvi = {http://gallium.inria.fr/~remy/ftp/control.dvi.gz},
  hideps = {http://gallium.inria.fr/~remy/ftp/control.ps.gz},
  pdf = {http://gallium.inria.fr/~remy/ftp/control.pdf},
  also = {http://gallium.inria.fr/~remy/work/cupto/},
  soft = {http://gallium.inria.fr/~remy/work/cupto/}
}
@unpublished{Remy/fool7,
  author = {Didier R{\'e}my},
  title = {Re-exploring multiple inheritance},
  note = {Invited talk at FOOL'7},
  year = 2000,
  month = jan,
  category = {D}
}
@unpublished{Remy-Vouillon/virtual-types,
  author = {Didier R{\'e}my and J{\'e}r{\^o}me Vouillon},
  title = {The reality of virtual types for free!},
  year = 1998,
  month = {October},
  note = {Unpublished note avaliable electronically},
  category = {D},
  abstract = { We show, mostly through detailed examples, that
                  programming patterns known to involve the notion of
                  virtual types can be implemented in a real object-oriented
                  language ---Ocaml--- in a direct way by taking advantage
                  of parametric classes and a flexible treatment of object
                  types via the use of row variables.  We also attempt to
                  explain the essence of virtual types.  Our \emph {free}
                  solution to virtual types seems to be more general and
                  often more flexible than \emph {ad hoc} solutions that
                  have been previously proposed.  },
  ps = {http://gallium.inria.fr/~remy/work/virtual/virtual.ps.gz},
  http = {http://gallium.inria.fr/~remy/work/virtual/}
}
@phdthesis{Remy/habilitation,
  author = {Didier R{\'e}my},
  title = {Des enregistrements aux objets},
  type = {M{\'e}moire d'habilitation {\`a} diriger des recherches},
  school = {Universit{\'e} de Paris~7},
  category = {D},
  year = 1998,
  abstract = { Les enregistrements, produits {\`a} champ nomm{\'e}s,
                  sont une structure simple et fondamentale en
                  programmation, et sont pr{\'e}sents depuis longtemps dans
                  de nombreux langages. Toutefois, certaines op{\'e}rations
                  sur les enregistrements, comme l'ajout de champs, restent
                  d{\'e}licates dans un langage fortement typ{\'e}.  Les
                  objets sont, au contraire, un concept tr{\`e}s
                  {\'e}volu{\'e}, expressif, mais les difficult{\'e}s {\`a}
                  les typer ou {\`a} les coder dans un lambda-calcul
                  typ{\'e} semblent refl{\'e}ter une complexit{\'e}
                  intrins{\`e}que.  \\ Une technique simple et
                  g{\'e}n{\'e}rale permet d'{\'e}tendre le typage des
                  enregistrements aux op{\'e}rations les plus avanc{\'e}es,
                  telles que l'acc{\`e}s polymorphe, l'extension, la
                  possibilit{\'e} d'avoir des valeurs par d{\'e}faut et une
                  forme de concat{\'e}nation. En ajoutant {\`a} ces
                  op{\'e}rations des types existentiels, objets et classes
                  deviennent directement programmables, sans sacrifice pour
                  leur expressivit{\'e}, mais au d{\'e}triment de la
                  lisibilit{\'e} des types synth{\'e}tis{\'e}s.  \\ Une
                  extension de ML avec des objets primitifs, Objective ML,
                  {\`a} la base de la couche objet du langage Ocaml, est
                  alors propos{\'e}e.  L'utilisation de constructions
                  primitives permet, en particulier, l'abr{\'e}viation
                  automatique des types qui rend l'interface avec
                  l'utilisateur conviviale.  Une extension harmonieuse du
                  langage avec des m{\'e}thodes polymorphes est
                  {\'e}galement possible.  \\ Tout en expliquant
                  l'imbrication entre les enregistrements, les objets et
                  classes, ces travaux montrent surtout que le polymorphisme
                  de ML, un concept simple et fondamental suffit {\`a}
                  rendre compte des op{\'e}rations les plus complexes sur
                  les objets.  La simplicit{\'e} et la robustesse
                  d'Objective ML et de son m{\'e}canisme de typage, qui ne
                  sacrifient en rien l'expressivit{\'e}, contribuent {\`a}
                  d{\'e}mystifier la programmation avec objets, et la
                  rendent accessible en toute s{\'e}curit{\'e} {\`a}
                  l'utilisateur, m{\^e}me novice.  },
  hideps = {http://gallium.inria.fr/~remy/ftp/habil.ps.gz},
  pdf = {http://gallium.inria.fr/~remy/ftp/habil.pdf}
}
@unpublished{Remy/classes-to-objects,
  author = {Didier R{\'e}my},
  title = {From Classes to Objects via Subtyping},
  note = {A preliminary version appeared in LNCS 1381 (ESOP 98)},
  year = 1998,
  month = {June},
  category = {D},
  abstract = { We extend the Abadi-Cardelli calculus of primitive
                  objects with object extension. We enrich object types with
                  a more precise, uniform, and flexible type structure.
                  This enables to type object extension under both width and
                  depth subtyping.  Objects may also have extend-only or
                  virtual contra-variant methods and read-only co-variant
                  methods.  The resulting subtyping relation is richer, and
                  types of objects can be weaken progressively from a class
                  level to a more traditional object level along the subtype
                  relationship.  },
  hidedvi = {http://gallium.inria.fr/~remy/ftp/classes-to-objects.dvi.gz},
  hideps = {http://gallium.inria.fr/~remy/ftp/classes-to-objects.ps.gz},
  pdf = {http://gallium.inria.fr/~remy/ftp/classes-to-objects.pdf}
}
@unpublished{Remy/sub-concat,
  author = {Didier R{\'e}my},
  title = {A case study of typechecking with constrained types:
                  Typing record concatenation},
  note = {Presented at the workshop on Advances in types for
                  computer science at the Newton Institute, Cambridge, UK},
  year = 1995,
  month = {August},
  category = {D},
  abstract = { We study static type-soundness of type systems with
                  non-atomic-subtyping based on constrained types for
                  first-order lambda-calculus (no Let) with one-field
                  records given with a call-by-value reduction semantics.
                  We then extend the language with general records with
                  concatenation.  This case study shows the flexibility of
                  type inference with constrained types.  We extend the
                  constrained types with type operators in order to
                  type-check record concatenation in the presence of
                  subtyping.  This method should provide wrappers to
                  object-oriented languages based on the
                  objects-as-records-of-methods paradigm.  We do not address
                  the practical issues of type inference here.  },
  dvi = {http://gallium.inria.fr/~remy/work/sub-concat.dvi.gz}
}
@unpublished{Remy/better-subtypes,
  author = {Didier R{\'e}my},
  title = {Better subtypes and row variables for record types},
  note = {Presented at the workshop on Advances in types for
                  computer science at the Newton Institute, Cambridge, UK},
  year = 1995,
  month = aug,
  category = {D},
  abstract = { In this note we compare row variables and subtypes for
                  record types.  We show that they are orthogonal to one
                  another and that record types benefit from having both at
                  the same time.  We proposed a unifying framework of record
                  types, and show that the several advantages of using an
                  enriched latice of subtypes for record types, in
                  particular this allows for extensible objects in the
                  presence of subtyping.  },
  dvi = {http://gallium.inria.fr/~remy/work/record_types.dvi.gz}
}
@unpublished{Pierce-Remy-Turner/pict,
  author = {Benjamin C. Pierce and Didier R{\'e}my and David
                  N. Turner},
  title = {A Typed Higher-Order Programming Language Based on the
                  Pi-Calculus},
  month = jul,
  year = 1993,
  category = {D},
  note = {A preliminary version was presented at the Workshop on
                  Type Theory and its Application to Computer Systems, Kyoto
                  University}
}
@techreport{Gunter-Remy/ravl,
  author = {Carl A.~Gunter and Didier R{\'e}my},
  title = {A proof-theoretic assessment of runtime type errors},
  institution = {AT\&T Bell Laboratories},
  year = 1993,
  type = {Research Report},
  number = {11261-921230-43TM},
  address = {600 Mountain Ave, Murray Hill, NJ 07974-2070},
  category = {D},
  abstract = { We analyze the way in which a result concerning the
                  absence of runtime type errors can be expressed when the
                  semantics of a language is described using proof rules in
                  what is sometimes called a natural semantics. We argue
                  that the usual way of expressing such results has
                  conceptual short-comings when compared with similar
                  results for other methods of describing semantics. These
                  short-comings are addressed through a form of operational
                  semantics based on proof rules in what we call a partial
                  proof semantics. A partial proof semantics represents
                  steps of evaluation using proofs with logic variables and
                  subgoals. Such a semantics allows a proof-theoretic
                  expression of the absence of runtime type errors that
                  addresses the problems with such results for natural
                  semantics. We demonstrate that there is a close
                  correspondence between partial proof semantics and a form
                  of structural operational semantics that uses a grammar to
                  describe evaluation contexts and rules for the evaluation
                  of redexes that may appear in such contexts. Indeed,
                  partial proof semantics can be seen as an intermediary
                  between such a description and one using natural
                  semantics. Our study is based on a case treatment for a
                  language called RAVL for Records And Variants Language,
                  which has a polymorphic type system that supports flexible
                  programming with records and variants.  },
  hidedvi = {http://gallium.inria.fr/~remy/ftp/ravl.dvi.gz},
  hideps = {http://gallium.inria.fr/~remy/ftp/ravl.ps.gz},
  pdf = {http://gallium.inria.fr/~remy/ftp/ravl.pdf}
}
@inproceedings{Remy/ml92,
  author = {Didier R{\'e}my},
  title = {Efficient Representation of Extensible Records},
  booktitle = {Proceedings of the 1992 workshop on {ML} and its
                  Applications},
  year = 1992,
  pages = 12,
  address = {San Francisco, USA},
  month = {June},
  hidedvi = {http://gallium.inria.fr/~remy/ftp/eff-repr-of-ext-records.dvi.gz},
  hideps = {http://gallium.inria.fr/~remy/ftp/eff-repr-of-ext-records.ps.gz},
  pdf = {http://gallium.inria.fr/~remy/ftp/eff-repr-of-ext-records.pdf},
  category = {D}
}
@techreport{Remy/mleth,
  author = {Didier R{\'e}my},
  title = {Extending {ML} Type System with a Sorted Equational
                  Theory},
  institution = {Institut National de Recherche en Informatique et
                  Automatisme},
  address = {Rocquencourt, BP 105, 78 153 Le Chesnay Cedex, France},
  type = {Research Report},
  number = 1766,
  year = 1992,
  category = {D},
  abstract = { We extend the ML language by allowing a sorted regular
                  equational theory on types for which unification is
                  decidable and unitary. We prove that the extension keeps
                  principal typings and subject reduction. A new set of
                  typing rules is proposed so that type generalization is
                  simpler and more efficient. We consider typing problems as
                  general unification problems, which we solve with a
                  formalism of unificands. Unificands naturally deal with
                  sharing between types and lead to a more efficient type
                  inference algorithm. The use of unificands also simplifies
                  the proof of correctness of the algorithm by splitting it
                  into more elementary steps.  },
  hidedvi = {http://gallium.inria.fr/~remy/ftp/eq-theory-on-types.dvi.gz},
  hideps = {http://gallium.inria.fr/~remy/ftp/eq-theory-on-types.ps.gz},
  pdf = {http://gallium.inria.fr/~remy/ftp/eq-theory-on-types.pdf}
}
@unpublished{Remy/type-systems@mpri2008,
  author = {Didier R{\'e}my},
  title = {{T}ype {S}ystems for {P}rogramming {L}anguages},
  note = {Course notes, available electronically},
  url = {http://gallium.inria.fr/~remy/poly/system/camlunix/cours.pdf},
  year = 2015,
  category = {D}
}
@unpublished{Leroy-Remy/system@poly2008,
  author = {Xavier Leroy and Didier R{\'e}my},
  title = {Programmation du syst{\`e}me {Unix} en {OCaml}},
  note = {Course notes, available electronically},
  url = {http://gallium.inria.fr/~remy/poly/system/camlunix/cours.pdf},
  year = 2008,
  category = {D}
}
@techreport{Remy/start,
  author = {Didier R{\'e}my},
  title = {Syntactic Theories and the Algebra of Record Terms},
  institution = {Institut National de Recherche en Informatique et
                  Automatisme},
  address = {Rocquencourt, BP 105, 78 153 Le Chesnay Cedex, France},
  type = {Research Report},
  number = 1869,
  year = 1993,
  category = {D},
  abstract = { Many type systems for records have been proposed. For
                  most of them, the types cannot be described as the terms
                  of an algebra. In this case, type checking, or type
                  inference in the case of first order type systems, cannot
                  be derived from existing algorithms. We define record
                  terms as the terms of an equational algebra. We prove
                  decidability of the unification problem for records terms
                  by showing that its equational theory is syntactic. We
                  derive a complete algorithm and prove its termination. We
                  define a notion of canonical terms and approximations of
                  record terms by canonical terms, and show that
                  approximations commute with unification. We also study
                  generic record terms, which extend record terms to model a
                  form of sharing between terms. We prove the syntacticness
                  of the equational theory of generic record terms and the
                  termination of the corresponding unification algorithm.  },
  hidedvi = {http://gallium.inria.fr/~remy/ftp/record-algebras.dvi.gz},
  hideps = {http://gallium.inria.fr/~remy/ftp/record-algebras.ps.gz},
  pdf = {http://gallium.inria.fr/~remy/ftp/record-algebras.pdf}
}
@techreport{Remy/records91,
  author = {Didier R{\'e}my},
  title = {Type Inference for Records in a natural Extension of {ML}},
  institution = {Institut National de Recherche en Informatique et
                  Automatisme},
  year = 1991,
  type = {Research Report},
  number = 1431,
  address = {Rocquencourt, BP 105, 78 153 Le Chesnay Cedex, France},
  month = may,
  note = {See also \cite{Remy/records} and \cite{Remy/popl89}.},
  hidedvi = {http://gallium.inria.fr/~remy/ftp/type-inf-records.dvi.gz},
  hideps = {http://gallium.inria.fr/~remy/ftp/type-inf-records.ps.gz},
  pdf = {http://gallium.inria.fr/~remy/ftp/type-inf-records.pdf},
  category = {D}
}
@phdthesis{Remy/thesis,
  author = {Didier R{\'e}my},
  title = {Alg{\`e}bres Touffues. Application au Typage Polymorphe
                  des Objets Enregistrements dans les Langages Fonctionnels},
  type = {Th{\`e}se de doctorat},
  school = {Universit{\'e} de Paris~7},
  year = 1990,
  hideps = {http://gallium.inria.fr/~remy/ftp/these.ps.gz},
  pdf = {http://gallium.inria.fr/~remy/ftp/these.pdf},
  category = {D}
}

This file was generated by bibtex2html 1.97.