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