@string {myself = "Didier R{\'{e}}my"}
@string {journal = "A"}
@string {book = "B"}
@string {bookchapter = "B"}
@string {conference = "C"}
@string {researchreport = "D"}
@string {talk = "D"}
@string {unpublished = "D"}
@string {dissertation = "D"}
@string {extendedversion = "D"}
@string {workshop = "D"}
@string {coursenotes = "D"}
@string{ftprocq = "http://gallium.inria.fr/~remy/ftp/"}
@string{fpottier = "http://gallium.inria.fr/~fpottier/publis/"}
@string{gallium = "http://gallium.inria.fr/~remy/"}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% hal-00934408, version 1
%% http://hal.inria.fr/hal-00934408
@unpublished{Remy-Scherer!sing@long2015,
author = {Gabriel Scherer and Didier R{\'{e}}my},
title = {Which simple types have a unique inhabitant?},
year = {2015},
category = unpublished,
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 = conference,
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 = conference,
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 = researchreport,
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 = workshop,
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 = workshop,
}
@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 = unpublished,
}
@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 = conference,
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 = researchreport,
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 = conference,
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 = unpublished,
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 = conference,
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 = unpublished,
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 = conference,
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 = journal,
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 = journal,
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 = bookchapter,
}
@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 = bookchapter,
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 = gallium # {cours/appsem/ocaml.ps.gz},
pdf = gallium # {cours/appsem/ocaml.pdf},
url = gallium # {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 = ftprocq # {iandc.dvi.gz},
hideps = ftprocq # {iandc.ps.gz},
pdf = ftprocq # {iandc.pdf},
category = journal,
}
@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 = journal,
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 = ftprocq # {objective-ml!tapos98.dvi.gz},
hideps = ftprocq # {objective-ml!tapos98.ps.gz},
pdf = ftprocq # {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 = journal,
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 = ftprocq # {dynamics.ps.gz},
pdf = ftprocq # {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 = bookchapter,
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 = ftprocq # {taoop1.dvi.gz},
hideps = ftprocq # {taoop1.ps.gz},
pdf = ftprocq # {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 = bookchapter,
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 = ftprocq # {taoop2.dvi.gz},
hideps = ftprocq # {taoop2.ps.gz},
pdf = ftprocq # {taoop2.pdf}
}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% http = {Conference papers},
%% tex = {\iffrench Articles de conf{\'e}rence\else
%% Papers in refereed conferences\fi}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Conferences
@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 = conference,
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 = conference,
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 = conference,
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 = conference,
also = gallium # {work/fml},
ps = gallium # {work/fml/fml-icfp.ps.gz},
pdf = gallium # {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 = fpottier # {dicosmo-pottier-remy-tlca05.ps.gz},
pdf = fpottier # {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 = conference,
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 = conference,
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 = conference,
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 = conference,
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 = conference,
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 = ftprocq # {tacs97.dvi.gz},
hideps = ftprocq # {tacs97.ps.gz},
pdf = ftprocq # {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 = conference,
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 = ftprocq # {objective-ml!popl97.dvi.gz},
hideps = ftprocq # {objective-ml!popl97.ps.gz},
pdf = ftprocq # {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 = conference,
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 = ftprocq # {typing-join.dvi.gz},
hideps = ftprocq # {typing-join.ps.gz},
pdf = ftprocq # {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 = conference,
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 = ftprocq # {mobile-agents.ps.gz},
pdf = ftprocq # {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 = conference,
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 = ftprocq # {prompt.dvi.gz},
hideps = ftprocq # {prompt.ps.gz},
pdf = ftprocq # {prompt.pdf},
http = gallium # {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 = conference,
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 = ftprocq # {tacs94.dvi.gz},
urlpublisher= {http://www.springerlink.com/index/p7136401k626j726.pdf},
hideps = ftprocq # {tacs94.ps.gz},
pdf = ftprocq # {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 = conference,
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 = ftprocq # {lfp92.dvi.gz},
hideps = ftprocq # {lfp92.ps.gz},
pdf = ftprocq # {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 = ftprocq # {free-concatenation.dvi.gz},
hideps = ftprocq # {free-concatenation.ps.gz},
pdf = ftprocq # {free-concatenation.pdf},
category = conference,
}
@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 = conference,
}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% http = {Other material},
%% tex = {\iffrench Autres publications\else
%% Other publications\fi}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Others
%% inria-00582570, version 2
%% http://hal.inria.fr/inria-00582570/en/
@techreport{Cretin-Remy:coercions@inria2011,
category = researchreport,
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 = unpublished,
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 = workshop,
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 = researchreport,
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 = unpublished,
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 = extendedversion,
}
@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 = unpublished,
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 = ftprocq # {control.dvi.gz},
hideps = ftprocq # {control.ps.gz},
pdf = ftprocq # {control.pdf},
ALSO = gallium # {work/cupto/},
SOFT = gallium # {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 = talk,
}
@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 = unpublished,
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 = gallium # {work/virtual/virtual.ps.gz},
http = gallium # {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 = dissertation,
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 = ftprocq # {habil.ps.gz},
pdf = ftprocq # {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 = extendedversion,
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 = ftprocq # {classes-to-objects.dvi.gz},
hideps = ftprocq # {classes-to-objects.ps.gz},
pdf = ftprocq # {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 = unpublished,
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 = gallium # {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 = unpublished,
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 = gallium # {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 = unpublished,
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 = researchreport,
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 = ftprocq # {ravl.dvi.gz},
hideps = ftprocq # {ravl.ps.gz},
pdf = ftprocq # {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 = ftprocq # {eff-repr-of-ext-records.dvi.gz},
hideps = ftprocq # {eff-repr-of-ext-records.ps.gz},
pdf = ftprocq # {eff-repr-of-ext-records.pdf},
category = workshop,
}
@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 = researchreport,
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 = ftprocq # {eq-theory-on-types.dvi.gz},
hideps = ftprocq # {eq-theory-on-types.ps.gz},
pdf = ftprocq # {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 = coursenotes,
}
@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 = coursenotes,
}
@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 = researchreport,
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 = ftprocq # {record-algebras.dvi.gz},
hideps = ftprocq # {record-algebras.ps.gz},
pdf = ftprocq # {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 = ftprocq # {type-inf-records.dvi.gz},
hideps = ftprocq # {type-inf-records.ps.gz},
pdf = ftprocq # {type-inf-records.pdf},
category = researchreport,
}
@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 = ftprocq # {these.ps.gz},
pdf = ftprocq # {these.pdf},
category = dissertation,
}