Publications available online 
Ma Qin and Luc Maranget, "Expressive Synchronization Types for Inheritance in the Join Calculus" 
In prior work, Fournet et al. proposed an extension of the join calculus with classbased inheritance, aiming to provide a precise semantics for concurrent objects. However, as we show here, their system suffers from several limitations, which make it inadequate to form the basis of a practical implementation. 
Cédric Fournet, Cosimo Laneve, Luc Maranget and Didier Rémy, "Inheritance in the Join Calculus", Conference Foundations of Software Technology and Theoretical Computer Science, 2000 
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.@inproceedings {FournetLaneveMarangetRemy!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", pdf= {http://cristal.inria.fr/~remy/work/ojoin/ojoin.pdf}, html= {http://cristal.inria.fr/~remy/work/ojoin/} } 
Ma Qin and Luc Maranget, "Compiling PatternMatching in JoinPatterns", 15th International Conference on Concurrency Theory (CONCUR 2004) 
We propose an extension of the joincalculus with pattern matching on algebraic data types. Our initial motivation is twofold: to provide an intuitive semantics of the interaction between concurrency and pattern matching; to define a practical compilation scheme from extended joindefinitions into ordinary ones plus ML pattern matching. To assess the correctness of our compilation scheme, we develop a theory of the applied joincalculus, a calculus with valuepassing and value matching.@inproceedings{patternmatching04, author = "{Ma Qin} and Luc Maranget", title = "Compiling PatternMatching in JoinPatterns", booktitle = "Proc. of the 15th International Conference on Concurrency Theory", year = 2004, series = "LNCS", volume = 3170, publisher = "SpringerVerlag"} 
Cédric Fournet, Fabrice Le Fessant, Luc Maranget and Alain Schmitt, "JoCaml: a Language for Concurrent Distributed and Mobile Programming" 
In these lecture notes, we give an overview of concurrent, distributed, and mobile programming using JoCaml. JoCaml is an extension of the Objective Caml language. It extends OCaml with support for concurrency and synchronization, the distributed execution of programs, and the dynamic relocation of active program fragments during execution.@misc{fournetjocaml, author = "Cedric Fournet and Fabrice Le Fessant and Luc Maranget and Alan Schmitt", title = "JoCaml: a Language for Concurrent Distributed and Mobile Programming", booktitle = "Advanced Functional Programming: 4th International School, AFP 2002", editors = "Johan Jeuring, Simon Peyton Jones", year = 2003, series = "LNCS", volume = 2638, publisher = "SpringerVerlag"} 
Fabrice Le Fessant and Luc Maranget, "Compiling JoinPatterns", Workshop HLCL’98. 
The joincalculus is both a name passing calculus and a core language for concurrent and distributed programming. An essential part of its implementation is the compilation of joinpatterns. Joinpatterns define new channels and all the synchronizations they take part to at the same time. In this paper, we study the compilation of joinpatterns into deterministic finitestate automata, from both the semantical and practical point of view. In particular, we discuss the compilation choices made in our two implementations, the join compiler and the jocaml system. We also describe some optimizations, related technical problems, and a useful simplification addressing these problems.@article{joinpattern98, author = "{Fabrice Le Fessant and Luc Maranget}", title = "Compiling JoinPatterns", journal = "Electronic Notes in Computer Science", volume = 16, number = 2, year = 1998, publisher "Elsevier"} 
Cédric Fournet, Cosimo Laneve, Luc Maranget and Didier Rémy, "Implicit Typing à la ML for the joincalculus", Conference CONCUR’97. 
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.@inproceedings{jointyping97, author = "Cédric Fournet, Cosimo Laneve, Luc Maranget and Didier Rémy", title = "Implicit Typing à la ML for the joincalculus", booktitle = "Proc. of the 1997 8th International Conference on Concurrency Theory", year = 1997, publisher = "SpringerVerlag"} 
Cédric Fournet and Georges Gonthier and JeanJacques Lévy and Luc Maranget and Didier Rémy, "A Calculus of Mobile Agents", Conference CONCUR’96 
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.@inproceedings{ fournet96calculus, author = "C{\'e}dric Fournet and Georges Gonthier and JeanJacques L{\'e}vy and Luc Maranget and Didier R{\'e}my", title = "A Calculus of Mobile Agents", booktitle = "Proceedings of the 7th International Conference on Concurrency Theory ({CONCUR}'96)", publisher = "SpringerVerlag", pages = "406421", year = "1996"} 
Luc Maranget, "Compiling Pattern Matching to Good Decisions Trees", ML’2008 
We address the issue of compiling ML pattern matching to compact and efficient decisions trees. Traditionally, compilation to decision trees is optimized by (1) implementing decision trees as dags with maximal sharing; (2) guiding a simple compiler with heuristics. We first design new heuristics that are inspired by necessity, a concept from lazy pattern matching that we rephrase in terms of decision tree semantics. Thereby, we simplify previous semantic frameworks and demonstrate a straightforward connection between necessity and decision tree runtime efficiency. We complete our study by experiments, showing that optimizing compilation to decision trees is competitive with the optimizing match compiler of Maranget & Le Fessant (2001)@article{marangetml2008, author = "Luc Maranget", title = "Compiling Pattern Matching to Good Decision Trees", booktitle = "Workshop on the Language ML", year = 2008, month = September, publisher = "ACM Press" } 
Luc Maranget, "Warnings for pattern matching", JFP’07 
We examine the ML patternmatching anomalies of useless clauses and nonexhaustive matches. We state the definition of these anomalies, building upon pattern matching semantics, and propose a simple algorithm to detect them. We have integrated the algorithm in the Objective Caml compiler, but we show that the same algorithm is also usable in a nonstrict language such as Haskell. Orpatterns are considered for both strict and nonstrict languages.@article{warnjfp07, author = "Luc Maranget", title = "Warnings for pattern matching", journal = "Journal of Functional Programming", volume = 17, issue = 03, year = 2007, month = May, publisher = "Cambridge University Press"} 
Luc Maranget, "Les avertissements du filtrage", JFLA’03 
Cet article propose une définition intrinsèque des anomalies de filtrage de ML que sont la clause inutile et le filtrage nonexhaustif, ainsi qu’un algorithme permettant de les signaler au programmeur.@inproceedings{warnjfla203, author = "Luc Maranget", title = "Les avertissements du filtrage", booktitle = "Actes des Journées Francophones des Langages Applicatifs", year = 2003, publisher = "Inria éditions"} 
Fabrice Le Fessant and Luc Maranget, "Optimizing PatternMatching", ICFP’2001 
We present improvements to the backtracking technique of patternmatching compilation. Several optimizations are introduced, such as commutation of patterns, use of exhaustiveness information, and control flow optimization through the use of labeled static exceptions and context information. These optimizations have been integrated in the ObjectiveCaml compiler. They have shown good results in increasing the speed of patternmatching intensive programs, without increasing final code size.@inproceedings{lefessantmaranget2001, author = "Fabrice {Le Fessant} and Luc Maranget", title = "Optimizing PatternMatching", booktitle = "Proceedings of the 2001 International Conference on Functional Programming ", year = 2001, publisher = "ACM Press"} 
Luc Maranget, "Two techniques for Compiling Lazy Pattern Matching" Research report 2385, INRIA, 1994. 
In ML style pattern matching, pattern size is not constrained and ambiguous patterns are allowed. This generality leads to a clear and concise programming style but is challenging in the context of lazy evaluation. A first challenge concerns language designers: in lazy ML, the evaluation order of expressions follows actual data dependencies. That is, only the computations that are needed to produce the final result are performed. Once given a proper (that is, nonambiguous) semantics, pattern matching should be compiled in a similar spirit: any value matching a given pattern should be recognized by performing only the minimal number of elementary tests needed to do so. This challenge was first met by A. Laville. A second challenge concerns compiler designers. As it stands, Laville’s compilation algorithm cannot be incorporated in an actual lazy ML compiler for efficiency and completeness reasons. As a matter of fact, Laville’s original algorithm did not fully treat the case of integers in patterns and can lead to explosions both in compilation time and generated code size. This paper provides a complete solution to that second challenge. In particular, the wellknown (and sizeefficient) pattern matching compilation technique using backtracking automata is here introduced for the first time into the world of lazy pattern matching. (If you are a specialist, see also a slightly improved, unpublished, version of this work)@techreport{MarangetLazyPatReport, author = "Luc Maranget", title = "Two Techniques for Compiling Lazy Pattern Matching", type = "Research report", number = "2385", institution = "INRIA", year = 1994} 
Luc Maranget, "Compiling Lazy Pattern Matching". Proceedings L&FP 92. 
In ML style pattern matching, pattern size is not constrained and ambiguous patterns are allowed. This generality leads to a clear and concise programming style but is challenging in the context of lazy evaluation. In lazy ML, the evaluation order of expressions follows actual data dependencies. That is, only the computations that are needed to produce the final result are performed. Once given a proper (that is, nonambiguous) semantics, pattern matching should be compiled in a similar spirit: any value matching a given pattern should be recognized by performing only the minimal number of elementary tests needed to do so. Starting from the A. Laville’s seminal work on the question, this paper gives a simple theoretical presentation of lazy pattern matching. It then introduces and proves a realistic compilation algorithm.@inproceedings{MarangetLazyPatConf, author = "Luc Maranget", title = "Compiling Lazy Pattern Matching", booktitle = "Proc. of the 1992 conference on Lisp and Functional Programming", year = 1992, publisher = "ACM Press"} 
JeanJacques Lévy and Luc Maranget, "Explicit Substitutions and Programming Languages", Invited paper Foundations of Software Technology and Theoretical Computer Science, 1999 
In this paper, we stress on the subtheory of weak substitutions, which is sufficient to analyze most of the properties of programming languages, and which preserves many of the nice theorems of the lambdacalculus. 
Thérèse Hardin, Luc Maranget and Bruno Pagano, "Functional BackEnds within the LambdaSigma Calculus", INRIA Research Report No 3034, 1996. 
This research report is a more thorough version of our homonymous ICFP’96 paper (see below). More specifically, the report proves the correctness of four abstract machines in great detail, whereas the article copes with two machines only. Please note that the report growed into a journal article: “Functional runtime systems within the lambdasigma calculus” that appeared in the Journal of Functional Programming 8(2), 131172, March 1998.@article{hardinmarangetpaganoreport, author = "Thérèse Hardin, Luc Maranget and Bruno Pagano", title = "Functional Runtimes within the LambdaSigma Calculus", journal = "Journal of Functional Programming", volume = 8, number = 2, month = March, year = 1998, publisher = "Cambridge University Press"} 
Thérèse Hardin, Luc Maranget and Bruno Pagano, "Functional BackEnds within the LambdaSigma Calculus", ICFP’96. 

Luc Maranget, "Optimal Derivations in Weak Lambdacalculi and in Orthogonal Term Rewriting Systems". Proceedings POPL’91. 
We introduce the new framework of Labeled Terms Rewriting Systems (TRS) a general framework to express sharing in Term Rewriting Systems (TRS). For Orthogonal Labeled TRS, an important subclass of Labeled TRS, we characterize optimal derivations. This result is applied to weak lambda calculi, showing the optimality of the lazy strategy, that is, the callbyname with sharing strategy. The result is also valid in the presence of deltarules, as in PCF. Orthogonal Labeled TRS is also useful as a calculus for proving syntactic properties of functional languages.@inproceedings{Marangetoptimality, author = "Luc Maranget", title = "Optimal Derivations in Orthogonal Term Rerwiting Systems and in Weak Lambda Calculi", booktitle = "Proc. of the 1991 conference on Principles of Programming Languages", year = 1991, publisher = "ACM Press"} 
Luc Maranget, "La stratégie paresseuse". Thèse de doctorat, Université de Paris 7, 1992 (in French). 
Les systèmes orthogonaux de réécriture sont étudiés en tant que modèle des langages de programmation. Dans cette approche, tout programme est représenté par un terme, ainsi que les éventuels résultats de l’évaluation de ce programme. On considère les résultats définitifs, ou formes normales, et divers types de résultats partiels, tels que les formes normales de tête. Les conditions d’orthogonalité assurent, pour un programme donné, l’unicité des résultats définitifs et intermédiaires qui sont donc bien définis. Les interpréteurs et compilateurs doivent ensuite suivre des méthodes ou stratégies de réduction pour calculer ces résultats. Des stratégies sont définies, puis étudiées, tant du point de vue de la correction —Si un programme admet un résultat, une stratégie correcte parvient à a calculer—, que de l’optimalité —Le calcul du résultat se fait en un nombre minimal d’étapes élémentaires—. La plus précise d’entre elles, la stratégie paresseuse, est correcte et optimale pour toutes les formes possibles de résultat. La mise en oeuvre effective de la stratégie paresseuse est finalement réalisée dans le cas du langage de programmation ML. L’appel par filtrage avec priorité de ML est complètement traité.@phdthesis{Marangetthese, author = "Luc Maranget", title = "La stratégie paresseuse", type = "Thèse de doctorat", school = "Université Paris 7", year = "1992"} 
Luc Maranget, "Functional satisfaction", Journal of Functional Programming (2004) 
This work presents simple decision procedures for the propositional calculus and for a simple predicate calculus. These decision procedures are based upon enumeration of the possible values of the variables in an expression. Yet, by taking advantage of the sequential semantics of boolean connectors, not all values are enumerated. In some cases, dramatic savings of machine time can be achieved. In particular, an equivalence checker for a small programming language appears to be usable in practice.@article{satisfaction04, author = "Luc Maranget" title = "Functional satisfaction", journal = "Journal of Functional Programming", volume = 14, number = 6, year = 2004, publisher = "Cambridge University Press"} 
Luc Maranget, "Hevea, un traducteur de LaTeX vers HTML en Caml", JFLA’99 
Cet article en français décrit l’architecture d’Hevea. Le traducteur Hevea est séparé en deux composants principaux : l’analyseur principal, qui reconnaît le source LaTeX, et le gestionnaire de sortie qui emet du HTML conforme à la spécification 3.2. Le traducteur exploite la similarité de structure entre les deux langages et reste simple. La reconnaissance et le rendu des équations mathématiques en HTML sont également abordées. Hevea reconnaît les définitions de commandes LaTeX. Cette particularité est permet à l’utlisateur de configurer Hevea facilement et en écrivant du source LaTeX. Hevea est écrit en Objective Caml, ses performances sont comparables avec celles du traducteur TTH qui est écrit en C.@inproceedings{hevea, author = "Luc Maranget", title = "Hevea, un traducteur de LaTeX vers HTML en Caml", booktitle = "Actes des 10èmes Journées francophones des langages applicatifs", year = 1999, publisher = "INRIA"} 
Luc Maranget, Gaml: a Parallel Implementation of Lazy ML, Proceedings FPCA’91. 
We present a new parallel implementation of lazy ML. Our scheme is a direct extension of the Gmachinebased implementation of lazy ML. Parallelism is introduced by fork annotations inserted by the programmer. We discuss the interference of such user annotations with strictness annotations generated by our compiler. The system has been implemented on a Sequent Balance computer. We also address the main practical issues involved, including stack and heap management.@inproceedings{Marangetgaml, author = "Luc Maranget", title = "Gaml: a Parallel Implementation of Lazy ML", booktitle = "Proc. of the 5th conference on Functional Programming and Computer Architecture", year = 1991, editor = "John Hugues", series = "LNCS", volume = 523, publisher = "SpringerVerlag"} 
This document was translated from L^{A}T_{E}X by H^{E}V^{E}A.