publications.bib

@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 = {C},
  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 = {B},
  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. 
},
  pdf = {coercions/Cretin-Remy!fmulti@draft2013.pdf},
  also = {http://gallium.inria.fr/~remy/coercions}
}
@inproceedings{Scherer:2013:GMS:2450268.2450309,
  author = {Scherer, Gabriel and R{\'e}my, Didier},
  title = {GADTs 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},
  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,
  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 = {B},
  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 = {A}
}
@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 = {A},
  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 = {A},
  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 = {A},
  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 = {B},
  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 = {B},
  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 = {B},
  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 = {B},
  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 = {B},
  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 = {B},
  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 = {B},
  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 = {B},
  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 = {B},
  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 = {B},
  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 = {B},
  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 = {B},
  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 = {B},
  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 = {B},
  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 = {B},
  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 = {B}
}
@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 = {B}
}
@techreport{Cretin-Remy:coercions@inria2011,
  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/PDF/full.pdf}
}
@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 = {C},
  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 = {C},
  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 = {C},
  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 = {C},
  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 = {C}
}
@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 = {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/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 = {C}
}
@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 = {C},
  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 = {C},
  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 = {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.
   },
  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 = {C},
  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 = {C},
  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 = {C},
  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 = {C},
  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 = {C}
}
@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 = {C},
  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}
}
@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 = {C},
  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 = {C}
}
@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 = {C}
}

This file was generated by bibtex2html 1.97.