Publications

We introduce the calculus of concurrent nets as an extension of the fusion calculus in which usual prefixing is replaced by arbitrary monotonic guards. Then we use this formalism to describe the prefixing policy of standard calculi as a particular form of communication. By developing a graphical syntax, we sharpen the geometric intuition and finally we provide an encoding of these guards as causality in the prefix-free fragment, in the spirit of the encoding of the fusion calculus into solos by Laneve and Victor, proving that communication by fusion is expressive enough to implement arbitrary monotonic guards.

@article{bm06:cnet,
    author = {Emmanuel Beffara and Fran\c{c}ois Maurel},
    title = {Concurrent Nets: a study of prefixing in process calculi},
    journal = {Theoretical Computer Science},
    volume = 356, number = 3, pages = {356--373},
    publisher = {Elsevier},
    year = 2006, month = may
}

We present an extension of the πI-calculus with formal sums of terms. A study of the properties of this sum reveals that its neutral element 0 can be used to make assumptions about the behaviour of the environment of a process. From this observation we derive an enriched calculus that enjoys a confluent reduction which preserves the testing semantics of processes. This system is shown to be strongly normalising for terms without replication, and the study of its normal forms provides fully abstract trace semantics for testing of πI processes.

@misc{bef08:apc,
    author = {Emmanuel Beffara},
    title = {An algebraic process calculus},
    booktitle = {Proceedings of the 33rd Annual IEEE Symposium on
      Logic in Computer Science (LICS 2008)},
    year = 2008, note = {To appear}
}

We build a realizability model for linear logic using a name-passing process calculus. The construction is based on testing semantics for processes, drawing ideas from spatial and modal logics, and yields a new type system for process calculi that ensures termination while allowing significantly concurrent behaviours. Then we study how embeddings of intuitionistic and classical logics into linear logic induce typed translations of λ and λμ-calculi in which new concurrent instructions can be introduced, thus sketching the basis for a Curry-Howard interpretation of linear and classical proofs in terms of concurrent interaction.

@inproceedings{bef05:cmll,
    author = {Emmanuel Beffara},
    title = {A Concurrent model for linear logic},
    booktitle = {Proceedings of the 21st Annual Conference on Mathematical
        Foundations of Programming Semantics (MFPS XXI)},
    series = {Electronic Notes in Theoretical Computer Science},
    volume = 155, pages = {147--168},
    publisher = {Elsevier},
    year = 2006, month = may
}

We introduce the calculus of concurrent nets as an extension of the fusion calculus in which usual prefixing is replaced by arbitrary monotonic guards. Then we use this formalism to describe the prefixing policy of standard calculi as a particular form of communication. By developing a graphical syntax, we sharpen the geometric intuition and finally we provide an encoding of these guards as causality in the prefix-free fragment, in the spirit of the encoding of the fusion calculus into solos by Laneve and Victor, proving that communication by fusion is expressive enough to implement arbitrary monotonic guards.

@inproceedings{bm04:cnet,
    author = {Emmanuel Beffara and Fran\c{c}ois Maurel},
    title = {Concurrent Nets: a study of prefixing in process calculi},
    booktitle = {Proceedings of the 11th International Workshop on
        Expressiveness in Concurrency (EXPRESS 2004)},
    series = {Electronic Notes in Theoretical Computer Science},
    volume = 128, number = 2, pages = {67--86},
    publisher = {Elsevier},
    year = 2005, month = apr
}

Within a classical call-by-name λ-calculus, we prove, using Krivine's realizability, that all terms typable with disjunctive normal forms (disjunctions of conjunctions of literals) share a common computational behaviour: they implement a multi-exception handling mechanism whose exact workings depend on the tautology. By using dynamic binding, we are able to define equivalent and more efficient primitive control combinators, which are neatly described through a specialized sequent calculus, and are correct in the sense that they realize the intended associated tautology.

@inproceedings{bd03:dnf,
    author = {Emmanuel Beffara and Vincent Danos},
    title = {Disjunctive Normal Forms and Local Exceptions},
    booktitle = {Proceedings of the Eigth ACM SIGPLAN
        International Conference on Functional Programming (ICFP 2003)},
    pages = {203--211},
    address = {Uppsala, Sweden},
    year = 2003, month = aug
}

We suggest and experimentally test a new approach to solving the parity games problem, equivalent to the propositional modal mu-calculus, a fundamental problem in automata, games, complexity theories, as well as in practical computer-aided verification, whose precise computational complexity is a long-standing open question. Based on the algorithm due to Gurvich, Karzanov, and Khachiyan for solving the more general mean payoff games, we make an adaptation and optimization for parity games, implement it in Knuth's system CWEB of ``literate programming'' using C++. The algorithm is less known in the model-checking community and is based on different ideas, as compared to the well-investigated ideas including fixpoint iteration, strategy improvement, dynamic programming. Run on a considerable number of randomly generated test game instances, the algorithm demonstrates a rapid convergence with sublinear number of iterations. Moreover, unlike other known algorithms, for which examples of exponential behaviors are known, our algorithm admits internal randomization, which gives improvements in our tests and may help the algorithm to avoid bad cases. Our experiments strongly suggest that the algorithm is polynomial on the average under reasonable distributions, which remains to be explained in further studies.

@techreport{bv01:gkk,
    author = {Emmanuel Beffara and Sergei Vorobyov},
    title = {Adapting {Gurvich-Karzanov-Khachiyan}'s Algorithm for Parity Games:
        Implementation and Experimentation},
    institution = {Department of Information Technology, Uppsala University},
    year = 2001,
    number = 020,
    note = {Short presentation at LICS'02}
}

ELAN is a powerful language and environment for specifying and prototyping deduction systems in a language based on rewrite rules controlled by strategies. Timed automata is a class of continuous real-time models of reactive systems for which efficient model-checking algorithms have been devised. In this paper, we show that these algorithms can very easily be prototyped in the ELAN system. This paper argues through this example that rewriting based systems relying on rules and strategies are a good framework to prototype, study and test rather efficiently symbolic model-checking algorithms, i.e. algorithms which involve combination of graph exploration rules, deduction rules, constraint solving techniques and decision procedures.

@inproceedings{bbkk01,
    author = {Emmanuel Beffara and Olivier Bournez and Hassen Kacem and Claude Kirchner},
    title = {Verification of timed automata using rewrite rules and strategies},
    booktitle = {Proceedings of BISFAI'01},
    address = {Ramat-Gan, Israel},
    editor = {Nachum Dershowitz and Ariel Frank},
    year = 2001, month = jun
}

This thesis is devoted to the application of realisability techniques in the study of the computational meaning of logic. In a first part, we recall the formalism of Krivine's classical realisability, in which we carry a study of the operational contents of purely classical tautologies. This exploration of the computational meaning of classical disjunction reveals rich behaviours, with strong interactive intuitions, that are profitably interpreted as typed control structures. In search of a better understanding of the nature of those mechanisms, we then define a similar realisability technique for a model of concurrent computation, in order to build a notion of constructivity that is not based on the idea of function, but rather on that of interactive process. The framework we get provides a genuinely concurrent interpretation of linear logic in a process calculus derived from the π-calculus, which allows us to apply in the concurrent case the specification methods previously studied in the sequential context. Subsequently, the study of translations of classical logic into linear logic provides systematic reconstructions of interactive decompositions of functional computation, which establishes a link at the logical level between the sequential and concurrent realisabilities. In the last part, we study in more detail the kind of computation inherited from process algebras, in order to understand its kind of scheduling. This study leads us to the definition of a more geometric computation model that allows a formal exploration of the notion of causality in concurrent calculi.

@phdthesis{bef05:lrc,
  author = {Beffara, Emmanuel},
  title = {Logique, r\'ealisabilit\'e et concurrence},
  school = {Universit\'e Paris 7},
	year = 2005, month = dec
}

This paper presents a non-interleaving denotational semantics for the π-calculus. The basic idea is to define a notion of test where the outcome is not only whether a given process passes a given test, but also in how many different ways it can pass it. More abstractly, the set of possible outcomes for tests forms a semiring, and the set of process interpretations appears as a module over this semiring, in which basic syntactic constructs are affine operators. This notion of test leads to a trace semantics in which traces are partial orders, in the style of Mazurkiewicz traces, extended with readiness information. Our construction has standard may- and must-testing as special cases.

We extend Krivine's classical realizability to a simply typed calculus with some constants and primitives and a call-with-current-continuation construct similar to Felleisen's C operator. We show how the theory extends smoothly by associating an appropriate truth value to concrete types. As a consequence, results and methods from realizability still hold in this new context; this is especially interesting in the case of specification theorems because they hold a significant meaning from the programmer's point of view.

@unpublished{b03:realconst,
    author = {Emmanuel Beffara},
    title = {Realizability with constants},
    year = 2003,
    note = {Workshop on Formal Methods and Security, Nanjing, China}
}

On commence par introduire le λκ-calcul, extension du λ-calcul avec contrôle, dont les règles de typage étendent la correspondance entre preuves et programmes à la logique propositionnelle classique. On rappelle ensuite le formalisme de la réalisabilité qui fournit des modèles de la logique propositionnelle permettant d'étudier le comportement calculatoire que spécifient les types. Dans ce cadre, on montre que certaines tautologies de la logique classique spécifient des mécanismes comparables à des structures de contrôle plus ou moins familières en programmation. De plus, on montre comment le calcul peut être enrichi par des combinateurs qui réalisent ces tautologies tout en faisant gagner de l'expressivité au calcul.

@misc{dea,
    author = {Emmanuel Beffara},
    title = {Tautologies classiques et combinateurs de contrôle},
    howpublished = {Mémoire de DEA},
    year = 2002, month = sep
}

@misc{mim2,
    author = {Emmanuel Beffara},
    title = {Adapting {Gurvich-Karzanov-Khachiyan}'s Algorithm for Parity Games:
        Implementation and Experimentation},
    howpublished = {Rapport de stage MIM2},
    year = 2001, month = aug
}

On s'intéresse ici à l'automatisation par la logique de réécriture de preuves de propriétés d'atteignabilité dans une forme d'automates temporisés. On commence pour cela par introduire un formalisme pour représenter des ensembles d'états du système. On construit ensuite à partir de ce formalisme un système de réécriture que l'on montre équivalent à l'automate considéré, puis on définit des stratégies destinées à rendre compte du fonctionnement de l'automate. On implémente enfin les méthodes de preuve établies à l'aide du logiciel ELAN pour montrer comment les preuves sont effectivement menées.

@misc{mim1,
    author = {Emmanuel Beffara},
    title = {Automates temporisés et calcul de réécriture},
    howpublished = {Rapport de stage MIM1},
    year = 2000, month = jul
}