2009
- [RY09]
-
Didier Rémy and Boris Yakobowski. A church-style intermediate language for MLF. Submitted, July 2009.
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 the call-by-value with the value-restriction. We exhibit a type preserving encoding of MLF into xMLF, which ensures type soundness for the most general version of MLF. We observe that xMLF is a calculus of retyping functions at the type level.
2008
- [Yak08b]
-
Boris Yakobowski. Le caractère ` à la rescousse - factorisation et réutilisation de code grâce aux variants polymorphes. In JFLA 2008 - Dix-neuvièmes Journées Francophones des Langages Applicatifs, pages 63-77, Étretat, January 2008. INRIA.
Les variants polymorphes sont une fonctionnalité puissante du système de types du langage OCaml, dont l'utilisation reste pourtant rare. Dans cet article, nous nous attachons à montrer en quoi ils sont plus expressifs que les types inductifs usuels, à la fois en terme de garantie statique d'invariants et de factorisation de code. Pour cela, nous proposons trois exemples tirés d'un typeur. Aucune connaissance préalable sur les variants polymorphes n'est nécessaire.
- [RY08]
-
Didier Rémy and Boris Yakobowski. From ML to MLF: Graphic type constraints with efficient type inference. In Proceedings of the 13th ACM SIGPLAN International Conference on Functional Programming (ICFP'08), Victoria, British Columbia, Canada, pages 63-74. ACM Press, September 2008.
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.
- [Yak08c]
- Boris Yakobowski. Types et contraintes graphiques : polymorphisme de second ordre et inférence. PhD thesis, Université Paris 7, December 2008.
- [Yak08a]
- Boris Yakobowski. Graphical types and constraints: second-order polymorphism and inference. PhD thesis, University Paris 7, December 2008.
2007
- [RY07]
-
Didier Rémy and Boris Yakobowski. A graphical presentation of MLF types with a linear-time unification algorithm. In TLDI'07: Proceedings of the 2007 ACM SIGPLAN International Workshop on Types in Languages Design and Implementation, pages 27-38, Nice, France, January 2007. ACM Press.
[ bib | Publisher | Details | pdf ]
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.
2005
- [WY05]
-
J. B. Wells and Boris Yakobowski. Graph-based proof counting and enumeration with applications for program fragment synthesis. In Sandro Etalle, editor, LOPSTR 2004: 14th International Symposium on Logic Based Program Synthesis and Transformation, LOPSTR 2004, Verona, Italy, August 26-28, 2004, Revised Selected Papers, volume 3573 of Lecture Notes in Computer Science, pages 262-277. Springer-Verlag, 2005.
[ bib | Publisher | Details | pdf | pdf (long version) ]
For use in earlier approaches to automated module interface adaptation, we seek a restricted form of program synthesis. Given some typing assumptions and a desired result type, we wish to automatically build a number of program fragments of this chosen typing, using functions and values available in the given typing environment. We call this problem term enumeration. To solve the problem, we use the Curry-Howard correspondence (propositions-as-types, proofs-as-programs) to transform it into a proof enumeration problem for an intuitionistic logic calculus. We formally study proof enumeration and counting in this calculus. We prove that proof counting is solvable and give an algorithm to solve it. This in turn yields a proof enumeration algorithm.
- [RY05]
- Dider Rémy and Boris Yakobowski. MLF with graphs. In APPSEM'05: Proceedings of the 3rd-APPSEM II Workshop on Applied Semantics, Frauenchiemsee, Germany, September 2005. Extended abstract.
2004
- [Yak04]
- Boris Yakobowski. Étude sémantique d'un langage intermédiaire de type Static Single Assignment. Rapport de dea (Master's thesis), ENS Cachan and INRIA Rocquencourt, September 2004. In french.
2002
- [Yak02]
- Boris Yakobowski. Module matching modulo isomorphisms. In WIT 2002, 1st International Workshop on Isomorphisms of Types, Toulouse, France, November 2002. Electronic proceedings at http://www.irit.fr/zeno/WIT2002/. In French.
