Publications available online

In prior work, Fournet et al. proposed an extension of the join calculus with class-based 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.

In this paper, we redesign the static semantics for inheritance in the join calculus, equipping class types with more precise information. Compared to previous work, the new type system is more powerful, more expressive and simpler. Additionally, one runtime check of the old system is suppressed in the new design. We also prove the soundness of the new system, and have implemented type inference (Springer web page).

@inproceedings{oojoin-typing03,
        author =  "{Ma Qin} and Luc Maranget",
        title = "Expressive Synchronization Types for Inheritance in the Join Calculus",
        booktitle = "Proc the First Asian Symposium on Programming Languages and Systems (APLAS'03)",
        year = 2003,
        series = "LNCS",
        volume = 2895,
        publisher = "Springer-Verlag",
        url = "http://www.springerlink.com/index/UQ32HTNNGWNXGU0U"
}

We propose an object-oriented calculus with internal concurrency and class-based 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   {Fournet-Laneve-Maranget-Remy!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/}
}

We propose an extension of the join-calculus 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 join-definitions into ordinary ones plus ML pattern matching. To assess the correctness of our compilation scheme, we develop a theory of the applied join-calculus, a calculus with value-passing and value matching.

@inproceedings{pattern-matching04,
        author =  "{Ma Qin} and Luc Maranget",
        title = "Compiling Pattern-Matching in Join-Patterns",
        booktitle = "Proc. of the 15th International Conference on Concurrency Theory",
        year = 2004,
        series = "LNCS",
        volume = 3170,
        publisher = "Springer-Verlag"}

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{fournet-jocaml,
  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 = "Springer-Verlag"}

The join-calculus 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 join-patterns. Join-patterns define new channels and all the synchronizations they take part to at the same time. In this paper, we study the compilation of join-patterns into deterministic finite-state 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{join-pattern-98,
        author =        "{Fabrice Le Fessant and Luc Maranget}",
        title =         "Compiling Join-Patterns",
        journal =       "Electronic Notes in Computer Science",
        volume = 16,
        number = 2,
        year =          1998,
        publisher       "Elsevier"}

We adapt the Damas-Milner typing discipline to the join-calculus. The main result is a new generalization criterion that extends the polymorphism of ML to join-definitions. We prove the correctness of our typing rules with regards to a chemical semantics. We also relate typed extensions of the core join-calculus to functional languages.

@inproceedings{join-typing-97,
        author =        "Cédric Fournet, Cosimo Laneve, Luc Maranget and Didier Rémy",
        title =         "Implicit Typing à la ML for the join-calculus",
        booktitle =     "Proc. of the 1997 8th International Conference on Concurrency Theory",
        year =          1997,
        publisher =     "Springer-Verlag"}

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 join-calculus.

@inproceedings{ fournet96calculus,
    author = "C{\'e}dric Fournet and Georges Gonthier and Jean-Jacques 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 = "Springer-Verlag",
    pages = "406--421",
    year = "1996"}

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{maranget-ml2008,
        author =        "Luc Maranget",
        title =         "Compiling Pattern Matching to Good Decision Trees",
        booktitle = "Workshop on the Language ML",
        year = 2008,
        month = September,
        publisher = "ACM Press"
}

We examine the ML pattern-matching anomalies of useless clauses and non-exhaustive 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 non-strict language such as Haskell. Or-patterns are considered for both strict and non-strict languages.

@article{warn-jfp-07,
        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"}

Cet article propose une définition intrinsèque des anomalies de filtrage de ML que sont la clause inutile et le filtrage non-exhaustif, ainsi qu’un algorithme permettant de les signaler au programmeur.

@inproceedings{warn-jfla203,
        author =        "Luc Maranget",
        title =         "Les avertissements du filtrage",
        booktitle =     "Actes des Journées Francophones des Langages Applicatifs",
        year =          2003,
        publisher =     "Inria éditions"}

We present improvements to the backtracking technique of pattern-matching 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 Objective-Caml compiler. They have shown good results in increasing the speed of pattern-matching intensive programs, without increasing final code size.

@inproceedings{lefessant-maranget-2001,
        author =        "Fabrice {Le Fessant} and Luc Maranget",
        title =         "Optimizing Pattern-Matching",
        booktitle =     "Proceedings of the 2001 International Conference on Functional Programming ",
        year =          2001,
        publisher =     "ACM Press"}

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, non-ambiguous) 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 well-known (and size-efficient) 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{Maranget-Lazy-Pat-Report,
        author =        "Luc Maranget",
        title =         "Two Techniques for Compiling Lazy Pattern Matching",
        type =          "Research report",
        number =        "2385",
        institution =   "INRIA",
        year =          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. 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, non-ambiguous) 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{Maranget-Lazy-Pat-Conf,
        author =        "Luc Maranget",
        title =         "Compiling Lazy Pattern Matching",
        booktitle =     "Proc. of the 1992 conference on Lisp and Functional
                         Programming",
        year =          1992,
        publisher =     "ACM Press"}

In this paper, we stress on the sub-theory 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 lambda-calculus.

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 lambda-sigma calculus” that appeared in the Journal of Functional Programming 8(2), 131-172, March 1998.

@article{hardin-maranget-pagano-report,
        author =        "Thérèse Hardin, Luc Maranget and Bruno Pagano",
        title =         "Functional Runtimes within the Lambda-Sigma Calculus",
        journal =       "Journal of Functional Programming",
        volume =        8,
        number =        2,
        month =         March,
        year  =         1998,
        publisher = "Cambridge University Press"}

We define a weak lambda-calculus, as a subsystem of the full lambda-calculus with explicit substitutions lambda-sigma-lift. We claim that our weak lambda-sigma-calculus could be the archetypal output language of functional compilers, just as the lambda-calculus is their universal input language. Furthermore, lambda-sigma-lift could be the adequate theory to establish the correctness of simplified functional compilers. Here, we illustrate these claims by proving the correctness of two simplified compilers and runtime systems modeled as abstract machines. We first present the Krivine machine. Then, we give the first formal proofs of Cardelli’s FAM and of its compiler.

x@inproceedings{hardin-maranget-pagano-96,
        author =        "Thérèse Hardin, Luc Maranget and Bruno Pagano",
        title =         "Functional Back-Ends within the Lambda-Sigma Calculus",
        booktitle =     "Proc. of the 1996 International Conference on Functional Programming",
        year =          1996,
        publisher =     "ACM Press"}

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 call-by-name with sharing strategy. The result is also valid in the presence of delta-rules, as in PCF. Orthogonal Labeled TRS is also useful as a calculus for proving syntactic properties of functional languages.

@inproceedings{Maranget-optimality,
        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"}

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{Maranget-these,
        author =        "Luc Maranget",
        title =         "La stratégie paresseuse",
        type =          "Thèse de doctorat",
        school =        "Université Paris 7",
        year =          "1992"}

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"}

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"}

We present a new parallel implementation of lazy ML. Our scheme is a direct extension of the G-machine-based 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{Maranget-gaml,
        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 =     "Springer-Verlag"}