Contact:

PPS
Université Denis Diderot
Case 7014
2 Place Jussieu
75251 PARIS Cedex 05 

email: montelapps.jussieu.fr
 

Ph.D. thesis

I also worked on the semantics of programming languages, by studying LLP (Linear Logics with Polarities) and its game models.
 

Papers and Reports

[Compilation]

• Objective Caml on .NET: The OCamIL Compiler and Toplevel, with Emmanuel Chailloux and Bruno Pagano, submitted, October 2004. 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.

• Interoperabilité des langages fonctionnels : applications en Objective Caml, with Emmanuel Chailloux and Grégoire Henry, submitted, June 2004.
• 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. (Postscript).

  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. (Compressed Postscript).

  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 with fixpoint.