@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.}, number = {{OOPSLA'24}}, url = {https://gallium.inria.fr/~remy/ocamod/}, pdf = {https://gallium.inria.fr/~remy/ocamod/Blaudeau-Remy-Radanne@oopsla24:fomt-extended.pdf}, year = 2024, note = {to appear}, category = {A} }

@article{DBLP:journals/pacmpl/BlaudeauL22, author = {Clement Blaudeau and Fengyun Liu}, title = {A conceptual framework for safe object initialization: a principled and mechanized soundness proof of the Celsius model}, journal = {Proc. {ACM} Program. Lang.}, volume = {6}, number = {{OOPSLA2}}, pages = {729--757}, year = {2022}, url = {https://doi.org/10.1145/3563314}, doi = {10.1145/3563314}, timestamp = {Mon, 28 Aug 2023 21:30:20 +0200}, biburl = {https://dblp.org/rec/journals/pacmpl/BlaudeauL22.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }

@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 = {{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 = {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}, 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}, 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.*