[1] 
Julien Cretin and Didier Rémy.
System F with Coercion Constraints.
Rapport de recherche RR8456, INRIA, January 2014.
[ bib 
PDF 
http ]
We present a secondorder lambdacalculus 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 equirecursive types. This allows to present in a uniform way several type system features that had previously been studied separately: type containment, bounded and instancebounded polymorphism, which are already encodable with parametric coercion abstraction, and MLstyle 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 evaluationand 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 abstractionsbut we also introduce a form of weak reduction as reduction cannot proceed under incoherent type abstractions. Type soundness is proved by adapting the stepindexed semantics technique to strong reduction strategies, moving indices inside terms so as to control the reduction steps internally.

[2] 
Jacques Garrigue and Didier Rémy.
Ambivalent Types for Principal Type Inference with
GADTs.
In 11th Asian Symposium on Programming Languages and Systems,
Melbourne, Australia, December 2013.
[ bib 
See also 
PDF ]
GADTs, short for Generalized Algebraic DataTypes, which allow constructors of algebraic datatypes to be nonsurjective, have many useful applications. However, pattern matching on GADTsintroduces local type equality assumptions, which are a source of ambiguities that may destroy principal typesand 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.

[3] 
Julien Cretin and Didier Rémy.
Coherent Coercion Abstration with a stepindexed
strongreduction semantics.
available at http://gallium.inria.fr/ remy/coercions/, July 2013.
[ bib 
See also 
PDF ]
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 secondorder 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 instancebounded polymorphism, as well as subtyping constraints as used for MLstyle type inference with subtyping. Type soundness is proved by adapting the stepindexed semantics technique to strong reduction strategies, moving indices inside terms so as to control the reduction steps internally.

[4] 
Gabriel Scherer and Didier Rémy.
GADTs Meet Subtyping.
In Proceedings of the 22Nd European Conference on Programming
Languages and Systems, ESOP'13, pages 554573, Berlin, Heidelberg, 2013.
SpringerVerlag.
[ bib 
DOI 
See also 
At Publisher's ]
While generalized abstract datatypes (GADT) are now considered wellunderstood, 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 finegrained 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 realworld MLlike languages with explicit subtyping such as OCaml, or to languages with general subtyping constraints.

[5] 
Jacques Garrigue and Didier Rémy.
Tracing ambiguity in GADT type inference.
Unpublished, June 2012.
[ bib 
PDF ]
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 typesand 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.

[6] 
Didier Rémy and Boris Yakobowski.
A ChurchStyle Intermediate Language for MLF.
Theoretical Computer Science, 435(1):77105, June 2012.
[ bib 
See also 
PDF 
At Publisher's ]
MLF is a type system that seamlessly merges MLstyle implicit but secondclass polymorphism with SystemF explicit firstclass polymorphism. We present xMLF, a Churchstyle 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 smallstep 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 weakreduction strategies, including callbyvalue with the valuerestriction.

[7] 
Julien Cretin and Didier Rémy.
On the Power of Coercion Abstraction.
In Proceedings of the 39th ACM Symposium on Principles of
Programming Languages (POPL 2012), Philadephia, PA, USA, January 2012.
[ bib 
See also 
At Publisher's ]
Erasable coercions in System Feta, also known as retyping functions, are welltyped etaexpansions of the identity. They may change the type of terms without changing their behavior and can thus be erased before reduction. Coercions in Feta can model subtyping of known types and some displacement of quantifiers, but not subtyping assumptions nor certain form of delayed type instantiation. We generalize Feta by allowing abstraction over retyping functions. We follow a general approach where computing with coercions can be seen as computing in the lambdacalculus 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 valueforms or by restricting abstraction to coercions that are polymorphic in their domain or codomain. The latter variant subsumes Feta, Fsub, and MLF in a unified framework.

[8] 
Julien Cretin and Didier Rémy.
Extending System Feta with Abstraction over Erasable
Coercions.
Research Report RR7587, INRIA, July 2011.
[ bib 
See also 
PDF 
At Publisher's ]
Erasable coercions in System Feta, also known as retyping functions, are welltyped etaexpansions of the identity. They may change the type of terms without changing their behavior and can thus be erased before reduction. Coercions in Feta can model subtyping of known types and some displacement of quantifiers, but not subtyping assumptions nor certain form of delayed type instantiation. We generalize Feta by allowing abstraction over retyping functions. We follow a general approach where computing with coercions can be seen as computing in the lambdacalculus 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 valueforms or by restricting abstraction to coercions that are polymorphic in their domain or codomain. The latter variant subsumes Feta, Fsub, and MLF in a unified framework.

[9] 
Didier Rémy and Boris Yakobowski.
A ChurchStyle Intermediate Language for MLF.
In Matthias Blume, Naoki Kobayashi, and German Vidal, editors,
Functional and Logic Programming, volume 6009 of Lecture Notes in
Computer Science, pages 2439. Springer Berlin / Heidelberg, 2010.
[ bib 
DOI 
See also 
PDF 
At Publisher's ]
MLF is a type system that seamlessly merges MLstyle implicit but secondclass polymorphism with SystemF explicit firstclass polymorphism. We present xMLF, a Churchstyle 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 smallstep 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 weakreduction strategies, including callbyvalue with the valuerestriction.

[10] 
Didier Le Botlan and Didier Rémy.
Recasting MLF.
Information and Computation, 207(6):726785, 2009.
[ bib 
DOI 
See also 
PDF 
At Publisher's 
http 
.ps.gz ]
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 designspace and expressiveness. We introduce a Currystyle version iMLF of MLF and provide an interpretation of iMLF types as instantiationclosed sets of SystemF types, from which we derive the definition of type instance in iMLF. We give equivalent syntactic definition of the typeinstance, presented as a set of inference rules. We also show an encoding of iMLF into the closure of Currystyle System F by letexpansion. We derive the Churchstyle 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. Keywords: ML 
[11] 
Benoît Montagu and Didier Rémy.
Modeling Abstract Types in Modules with Open Existential Types.
In Proceedings of the 36th ACM Symposium on Principles of
Programming Languages (POPL'09), pages 354365, Savannah, GA, USA, January
2009.
[ bib 
DOI 
See also 
PDF ]
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 smallstep 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 CurryHoward isomorphism, Fzip can be also read back as a logic with the same expressive power as secondorder 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 typelevel and termlevel 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.

[12] 
Didier Rémy and Boris Yakobowski.
Efficient Type Inference for the MLF Language: a
graphical and constraintsbased approach.
In The 13th ACM SIGPLAN International Conference on Functional
Programming (ICFP'08), pages 6374, Victoria, BC, Canada, September 2008.
[ bib 
DOI 
See also 
PDF ]
MLF is a type system that seamlessly merges MLstyle type inference with SystemF 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.

[13] 
Benoît Montagu and Didier Rémy.
Towards a Simpler Account of Modules and Generativity: Abstract
Types have Open Existential Types.
January 2008.
[ bib 
See also 
PDF ]
We present a variant of the explicitlytyped secondorder polymorphic lambdacalculus 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 callbyvalue smallstep 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.

[14] 
Didier Le Botlan and Didier Rémy.
Recasting MLF.
Research Report 6228, INRIA, Rocquencourt, BP 105, 78 153 Le Chesnay
Cedex, France, June 2007.
[ bib 
See also 
PDF 
At Publisher's ]
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 typeinstance 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.

[15] 
Didier Rémy and Boris Yakobowski.
A graphical presentation of MLF types with a lineartime
unification algorithm.
In Proceedings of the 2007 ACM SIGPLAN International Workshop on
Types in Languages Design and Implementation (TLDI'07), pages 2738, Nice,
France, January 2007. ACM Press.
[ bib 
http ]
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 termdag, encoding the underlying termstructure with sharing, and a binding tree encoding the bindingstructure. 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 firstorder terms. Moreover, it permits a simpler and more direct definition of type instance that combines type instance on firstorder termdags, simple operations on dags, and a control that allows or rejects potential instances. Using this representation, we build a lineartime unification algorithm for MLF types, which we prove sound and complete with respect to the specification.

[16] 
Didier Rémy and Boris Yakobowski.
A graphical presentation of MLF types with a lineartime
incremental unification algorithm.
Extended version of [15], July
2006.
[ bib 
See also 
PDF 
.ps.gz ]
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 termdag, encoding the underlying termstructure with sharing, and a binding tree, encoding the bindingstructure. This representation is more canonical as it factors out most of the notational details of the original definition; it is also closely related to firstorder terms. Moreover, it permits a simpler and more direct definition of type instance that combines typeinstance on firstorder termdags, simple operations on dags, and a control that allows or rejects potential instances. Thanks to this representation, we obtain an incremental lineartime 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.

[17] 
Didier Rémy.
Simple, partial typeinference for System F based on
typecontainment.
In Proceedings of the tenth International Conference on
Functional Programming, September 2005.
[ bib 
See also 
PDF 
.ps.gz ]
We explore partial typeinference for System F based on typecontainment. We consider both cases of a purely functional semantics and a callbyvalue stateful semantics. To enable typeinference, we require higherrank polymorphism to be userspecified via type annotations on source terms. We allow implicit predicative typecontainment and explicit impredicative typeinstantiation. 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 typereconstruction 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.

[18] 
Roberto Di Cosmo, François Pottier, and Didier Rémy.
Subtyping Recursive Types modulo Associative Commutative
Products.
In Seventh International Conference on Typed Lambda Calculi and
Applications (TLCA'05), Nara, Japan, April 2005.
[ bib 
Long version .pdf 
Long version 
PDF 
.ps.gz ]
This work sets the formal bases for building tools that help retrieve classes in objectoriented 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 productsthat is, subtyping modulo a restricted form of type isomorphismsas 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.

[19]  François Pottier and Didier Rémy. The Essence of ML Type Inference. In Benjamin C. Pierce, editor, Advanced Topics in Types and Programming Languages, chapter 10, pages 389489. MIT Press, 2005. [ bib  http ] 
[20] 
Didier Le Botlan and Didier Rémy.
MLF: Raising ML to the power of System F.
In Proceedings of the Eighth ACM SIGPLAN International
Conference on Functional Programming, pages 2738, August 2003.
[ bib 
PDF 
http 
.dvi.gz 
.ps.gz ]
We propose a type system MLF that generalizes ML with firstclass polymorphism as in System F. Expressions may contain secondorder 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 welltyped 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 lambdaabstractions into MLF types. Moreover, only parameters of lambdaabstractions that are used polymorphically need to remain annotated.

[21]  François Pottier and Didier Rémy. The Essence of ML Type Inference. Extended preliminary version of [19], 2003. [ bib  See also  .ps.gz ] 
[22] 
Didier Rémy.
Using, Understanding, and Unraveling the OCaml
Language.
In Gilles Barthe, editor, Applied Semantics. Advanced
Lectures. LNCS 2395., pages 413537. Springer Verlag, 2002.
[ bib 
PDF 
http 
.ps.gz ]
These course notes are addressed to a wide audience of people interested in modern programming languages in general, MLlike languages in particular, or simply in OCaml, whether they are programmers or language designers, beginners or knowledgeable readers little prerequiresite is actually assumed.

[23] 
Cédric Fournet, Luc Maranget, Cosimo Laneve, and Didier Rémy.
Inheritance in the Join Calculus.
In Foundations of Software Technology and Theoretical Computer
Science, volume 1974 of Lecture Notes in Computer Science. Springer,
December 2000.
[ bib 
PDF 
http 
.ps.gz ]
We propose an objectoriented calculus with internal concurrency and classbased 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.

[24]  Didier Rémy. Reexploring multiple inheritance. Invited talk at FOOL'7, January 2000. [ bib ] 
[25] 
Jacques Garrigue and Didier Rémy.
Extending ML with SemiExplicit HigherOrder Polymorphism.
Information and Computation, 155(1/2):134169, 1999.
A preliminary version appeared in TACS'97.
[ bib 
PDF 
http ]
We propose a modest conservative extension to ML that allows semiexplicit firstclass 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 semiimplicit: 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.

[26] 
Didier Rémy and Jérôme Vouillon.
The reality of virtual types for free!
Unpublished note avaliable electronically, October 1998.
[ bib 
http 
.ps.gz ]
We show, mostly through detailed examples, that programming patterns known to involve the notion of virtual types can be implemented in a real objectoriented 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 free solution to virtual types seems to be more general and often more flexible than ad hoc solutions that have been previously proposed.

[27] 
Didier Rémy.
From Classes to Objects via Subtyping.
A preliminary version appeared in LNCS 1381 (ESOP 98), June 1998.
[ bib 
PDF ]
We extend the AbadiCardelli 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 extendonly or virtual contravariant methods and readonly covariant 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.

[28] 
Didier Rémy.
From Classes to Objects via Subtyping.
In European Symposium On Programming, volume 1381 of
Lecture Notes in Computer Science. Springer, March 1998.
[ bib 
.html ]
We extend the AbadiCardelli 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 extendonly or virtual contravariant methods and readonly covariant 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.

[29] 
Didier Rémy and Jérôme Vouillon.
Objective ML: An effective objectoriented extension to ML.
Theory And Practice of Object Systems, 4(1):2750, 1998.
A preliminary version appeared in the proceedings of the 24th ACM
Conference on Principles of Programming Languages, 1997.
[ bib 
PDF ]
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 objectoriented 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.

[30] 
Carl A. Gunter, Didier Rémy, and Jon G. Riecke.
Return types for Functional Continuations.
A preliminary version appeared as [38],
1998.
[ bib 
Software 
See also 
PDF ]
We add functional continuations and prompts to a language with an MLstyle 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 welltyped terms never produce runtime type errors and give a module for implementing them in the latest version of SML/NJ.

[31] 
Didier Rémy.
Des enregistrements aux objets.
Mémoire d'habilitation à diriger des recherches,
Université de Paris 7, 1998.
[ bib 
PDF ]
Les enregistrements, produits à champ nommés, sont une structure simple et fondamentale en programmation, et sont présents depuis longtemps dans de nombreux langages. Toutefois, certaines opérations sur les enregistrements, comme l'ajout de champs, restent délicates dans un langage fortement typé. Les objets sont, au contraire, un concept très évolué, expressif, mais les difficultés à les typer ou à les coder dans un lambdacalcul typé semblent refléter une complexité intrinsèque.

[32] 
Jacques Garrigue and Didier Rémy.
Extending ML with SemiExplicit HigherOrder Polymorphism.
In International Symposium on Theoretical Aspects of Computer
Software, volume 1281 of Lecture Notes in Computer Science, pages
2046. Springer, September 1997.
[ bib 
PDF ]
We propose a modest conservative extension to ML that allows semiexplicit higherorder 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 semiimplicit: 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.

[33] 
Didier Rémy and Jérôme Vouillon.
Objective ML: A simple objectoriented extension of ML.
In Proceedings of the 24th ACM Conference on Principles of
Programming Languages, pages 4053, Paris, France, January 1997.
[ bib 
PDF ]
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 objectoriented 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.

[34] 
Cédric Fournet, Luc Maranget, Cosimo Laneve, and Didier Rémy.
Implicit typing à la ML for the joincalculus.
In 8th International Conference on Concurrency Theory
(CONCUR'97), volume 1243 of Lecture Notes in Computer Science, pages
196212, Warsaw, Poland, 1997. Springer.
[ bib 
PDF ]
We adapt the DamasMilner typing discipline to the joincalculus. The main result is a new generalization criterion that extends the polymorphism of ML to joindefinitions. We prove the correctness of our typing rules with regards to a chemical semantics. We also relate typed extensions of the core joincalculus to functional languages.

[35] 
Cédric Fournet, Georges Gonthier, JeanJacques Lévy, Luc Maranget, and
Didier Rémy.
A Calculus of Mobile Agents.
In 7th International Conference on Concurrency Theory
(CONCUR'96), volume 1119 of Lecture Notes in Computer Science, pages
406421, Pisa, Italy, August 2629 1996. Springer.
[ bib 
PDF ]
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 joincalculus. (BibTeX reference.)

[36] 
Didier Rémy.
A case study of typechecking with constrained types: Typing
record concatenation.
Presented at the workshop on Advances in types for computer science
at the Newton Institute, Cambridge, UK, August 1995.
[ bib 
.dvi.gz ]
We study static typesoundness of type systems with nonatomicsubtyping based on constrained types for firstorder lambdacalculus (no Let) with onefield records given with a callbyvalue 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 typecheck record concatenation in the presence of subtyping. This method should provide wrappers to objectoriented languages based on the objectsasrecordsofmethods paradigm. We do not address the practical issues of type inference here.

[37] 
Didier Rémy.
Better subtypes and row variables for record types.
Presented at the workshop on Advances in types for computer science
at the Newton Institute, Cambridge, UK, August 1995.
[ bib 
.dvi.gz ]
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.

[38] 
Carl A. Gunter, Didier Rémy, and Jon G. Riecke.
A Generalization of Exceptions and Control in ML.
In Proc. ACM Conf. on Functional Programming and Computer
Architecture, June 1995.
[ bib 
PDF 
http ]
We add functional continuations and prompts to a language with an MLstyle 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 welltyped terms never produce runtime type errors and give a module for implementing them in the latest version of SML/NJ.

[39] 
Martín Abadi, Luca Cardelli, Benjamin C. Pierce, and Didier Rémy.
Dynamic typing in polymorphic languages.
Journal of Functional Programming, 5(1):111130, January 1995.
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.
[ bib 
PDF ]
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.

[40] 
Didier Rémy.
Programming Objects with MLART: An extension to ML with
Abstract and Record Types.
In Masami Hagiya and John C. Mitchell, editors, International
Symposium on Theoretical Aspects of Computer Software, number 789 in Lecture
Notes in Computer Science, pages 321346, Sendai, Japan, April 1994.
SpringerVerlag.
[ bib 
PDF ]
Classbased 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 superclasses. 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 MLART is given with a callbyvalue semantics for which type soundness is proved.

[41]  Benjamin C. Pierce, Didier Rémy, and David N. Turner. A Typed HigherOrder Programming Language Based on the PiCalculus. A preliminary version was presented at the Workshop on Type Theory and its Application to Computer Systems, Kyoto University, July 1993. [ bib ] 
[42] 
Didier Rémy.
Type Inference for Records in a Natural Extension of ML.
In Carl A. Gunter and John C. Mitchell, editors, Theoretical
Aspects Of ObjectOriented Programming. Types, Semantics and Language
Design. MIT Press, 1993.
[ bib 
PDF ]
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.

[43] 
Didier Rémy.
Typing Record Concatenation for Free.
In Carl A. Gunter and John C. Mitchell, editors, Theoretical
Aspects Of ObjectOriented Programming. Types, Semantics and Language
Design. MIT Press, 1993.
[ bib 
PDF ]
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

[44] 
Carl A. Gunter and Didier Rémy.
A prooftheoretic assessment of runtime type errors.
Research Report 1126192123043TM, AT&T Bell Laboratories, 600
Mountain Ave, Murray Hill, NJ 079742070, 1993.
[ bib 
PDF ]
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 shortcomings when compared with similar results for other methods of describing semantics. These shortcomings 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 prooftheoretic 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.

[45] 
Didier Rémy.
Syntactic Theories and the Algebra of Record Terms.
Research Report 1869, Institut National de Recherche en Informatique
et Automatisme, Rocquencourt, BP 105, 78 153 Le Chesnay Cedex, France, 1993.
[ bib 
PDF ]
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.

[46]  Didier Rémy. Efficient Representation of Extensible Records. In Proceedings of the 1992 workshop on ML and its Applications, page 12, San Francisco, USA, June 1992. [ bib  PDF ] 
[47] 
Didier Rémy.
Projective ML.
In 1992 ACM Conference on Lisp and Functional Programming,
pages 6675, NewYork, 1992. ACM press.
[ bib 
PDF ]
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.

[48]  Didier Rémy. Typing Record Concatenation for Free. In Nineteenth Annual Symposium on Principles Of Programming Languages, pages 166176, 1992. [ bib  PDF ] 
[49] 
Didier Rémy.
Extending ML Type System with a Sorted Equational Theory.
Research Report 1766, Institut National de Recherche en Informatique
et Automatisme, Rocquencourt, BP 105, 78 153 Le Chesnay Cedex, France, 1992.
[ bib 
PDF ]
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.

[50]  Didier Rémy. Type Inference for Records in a natural Extension of ML. Research Report 1431, Institut National de Recherche en Informatique et Automatisme, Rocquencourt, BP 105, 78 153 Le Chesnay Cedex, France, May 1991. See also [42] and [52]. [ bib  PDF ] 
[51]  Didier Rémy. Algèbres Touffues. Application au Typage Polymorphe des Objets Enregistrements dans les Langages Fonctionnels. Thèse de doctorat, Université de Paris 7, 1990. [ bib  PDF ] 
[52]  Didier Rémy. Records and Variants as a natural Extension of ML. In Sixteenth Annual Symposium on Principles Of Programming Languages, 1989. See also [42]. [ bib ] 
This file was generated by bibtex2html 1.97.