Université Denis Diderot
2 Place Jussieu
75251 PARIS Cedex 05
Back to PPS homepage
I was a Ph.D. student in the PPS team at the Paris 7 University (advisor:
My research topics include compilation and interoperability.
I developed OCamIL,
a compiler of the Objective Caml language to
the .NET platform.
I also worked on the semantics of programming languages, by studying LLP (Linear Logics with Polarities) and its game models.
Papers and Reports
Functional languages, typing and interoperability: Objective Caml on .NET, PhD thesis, March 2007, (Compressed Postscript and Slides, both in French).
The .NET platform is a modern, widespread execution environment, based on a virtual machine that interprets a typed bytecode. It claims to be perfectly suitable for running components written in many different programming languages and to allow a seamless interoperation between them.
Being a statically typed functional language with parametric polymorphism, Objective Caml has features that are quite challenging to the .NET runtime and its type system. We test the fit in a practical setting by designing and implementing OCamIL, a full-fledged compiler for Objective Caml producing verifiable .NET bytecode. It primarily aims at compatibility and interoperability.
This work questions the capabilities of the .NET platform as much as the adequacy of the official Objective Caml implementation (which is designed for an untyped runtime and discards type information early in the compilation chain). We discuss the representation of Caml values and compare two strategies: rebuilding and propagating the missing type information. Other design choices described here illustrate the trade-off between efficiency and readibility/interoperability.
We achieve interoperability by means of an Interface Description Language that closes the gap between the two distinct class systems of Objective Caml and .NET's underlying type system. We give non-trivial examples showing the benefits of interoperability.
As for performance, OCamIL proves competitive with other .NET compilers for functional languages. We also compare .NET executables with the original Objective Caml programs.
Objective Caml on .NET: The OCamIL Compiler and Toplevel, with Emmanuel Chailloux and Bruno Pagano, in Proc. 3rd International Conference on .NET technologies, May 2005, (PDF).
Preliminary version available as: PPS Technical Report 29, April 2004. (PDF, Compressed Postscript).
We present the OCamIL compiler for Objective Caml that targets .NET.
Our experiment consists in adding a new back-end to the INRIA Objective Caml compiler, that generates MSIL bytecode.
Among all the advantages of code reuse, ensuring compatibility while keeping all the expressiveness of the original language
is particularly interesting.
This allowed us to bootstrap the OCamIL compiler as a .NET component and
build an interactive loop (toplevel) which may be embedded within .NET applications.
This work deals with typing issues, because OCamIL needs to translate an untyped intermediate language into
a typed bytecode.
We discuss various intermediate language retyping techniques and their consequences on performances.
We also present applications of interoperability of Objective Caml and C# components.
Interopérabilité des langages fonctionnels : applications en Objective Caml, with Emmanuel Chailloux and Grégoire Henry,
in Technique et Sciences Informatiques Vol 24/9 - 2005.
We present in this paper the evolution of the interoperability needs of the functional languages, illustrated in Objective Caml by our tools and multi-languages applications. First of all we describe the inherent difficulties of the low-level interfaces of communication for memory management and context switching. Then we define a new code generator, called O'Jacaré, designed to facilitate interoperation between Java and Objective Caml through their object models. O'Jacaré defines a basic IDL (Interface Definition Language) for classes and interfaces description to communicate from Objective Caml to Java. The adaptation of O'Jacaré to .NET, called O'Jacaré.net, improves communication between Objective Caml and C# via this common runtime.
Mixing the Objective Caml and C# Programming Models in the .NET Framework, with Emmanuel Chailloux and Grégoire Henry,
Int. Workshop on Multiparadigm Programming with OO Languages (MPOOL'04), June 2004. (PDF, Compressed Postscript).
We present a new code generator, called O'Jacaré.net, to inter-operate between C# and Objective Caml through their object models.
O'Jacaré.net defines a basic IDL (Interface Definition Language) that describes classes and interfaces in order
to communicate between Objective Caml and C#.
O'Jacaré.net generates all needed wrapper classes and takes advantage of static type checking in both worlds.
Although the IDL intersects these two object models, O'Jacaré.net allows to combine features from both.
OCamIL : un compilateur Objective Caml pour .NET, with Emmanuel Chailloux and Bruno Pagano,
in Proc. 2nd International Conference of Frenchspeaking and Vietnamese Computer Scientists (RIVF'04), February 2004.
We present a first version of our Objective Caml compiler, called OCamIL, for .NET. Our goal
is to understand whether this new generation of virtual machines and runtime environment can help us compile ML programs
and produce executables of reasonable efficiency. Our main constraint is to be compatible with the original
language, and its advanced programming features (functional values, exceptions, parameterized modules, objects).
[Proof nets and game semantics]
Polarized Proof Nets with Cycles and Fixpoints Semantics,
in Proc. 6th International Conference on Typed Lambda Calculi and Applications (TLCA 2003),
Springer LNCS 2701, pp 256-170, June 2003.
(PDF, Compressed Postscript).
Starting from Laurent's work on Polarized Linear Logic, we define a new polarized linear deduction system which handles recursion.
This is achieved by extending the cut rule, in such a way that iteration unrolling is achieved by cut-elimination.
The proof-nets counterpart of this extension is obtained by allowing oriented cycles, which had no meaning in usual polarized linear logic.
We also free proof nets from additional constraints, leading up to a correctness criterion as straightforward as possible
(since almost all proof structures are correct). Our system has a sound semantics expressed in traced models.
Présentation axiomatique de théorèmes
de complétude forte en sémantique des jeux et en logique
classique, master thesis,
under the supervision of Paul-André Melliès), September 2001.
We take an axiomatic approach in solving definabilty problems for Linear Logic with Polarities and the lambda-mu-calculus (with disjonction)
in continuation categories.
We then define a fixpoint-enabled version of Linear Logic with Polarities in order to extend our results to the lambda-mu-calculus