Emmanuel Beffara - Publications

A quantitative model of concurrent interaction is introduced. The basic objects are linear combinations of partial order relations, acted upon by a group of permutations that represents potential non-determinism in synchronisation. This algebraic structure is shown to provide faithful interpretations of finitary process algebras, for an extension of the standard notion of testing semantics, leading to a model that is both denotational (in the sense that the internal workings of processes are ignored) and non-interleaving. Constructions on algebras and their subspaces enjoy a good structure that make them (nearly) a model of differential linear logic, showing that the underlying approach to the representation of non-determinism as linear combinations is the same.

@techreport{bef11:oa,
  author = {Beffara, Emmanuel},
  title = {Order algebras: a quantitative model of interaction},
  institution = {Institut de Math\'ematiques de Luminy},
  type = {Technical report},
  number = {hal-00429610},
  note = {Available online at http://hal.archives-ouvertes.fr/hal-00429610/},
  month = jul,
  url = {http://hal.archives-ouvertes.fr/hal-00429610/},
  year = 2011
}

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.

@inproceedings{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)},
    pages = {130--141},
    year = 2008
}

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 proposes a new interpretation of the logical contents of programs in the context of concurrent interaction, wherein proofs correspond to successful executions of a processes. A type system based on linear logic is used, in which a given process may have several different types, each typing corresponding to a particular way of interacting with its environment, and cut elimination corresponds to executing the process in a given scenario. We prove that, for any process, the set of lock-avoiding executions precisely corresponds to the set of typings of the process. Particularly important is the role played by the axiom rule, which allows typings to make assumptions on the events of the environment. In this interpretation, logic appears as a way of making explicit the flow of causality between interacting processes.

@techreport{bm11:pae,
  author = {Beffara, Emmanuel and Mogbil, Virgile},
  title = {Proofs as executions},
  type = {Technical report},
  number = {hal-00586459},
  note = {Available online at http://hal.archives-ouvertes.fr/hal-00586459/},
  month = apr,
  url = {http://hal.archives-ouvertes.fr/hal-00586459/},
  year = 2011
}

We present a proofs-as-programs correspondence between linear logic and process calculi that permits non-deterministic behaviours. Processes are translated into wireless proof nets, i.e. proof nets of multiplicative linear logic without cut wires. Typing a term using them consists in typing some of its possible determinisations in standard sequent calculus. Generalized cut-elimination steps in wireless proof nets is shown to correspond to executions that avoid deadlocks.

@techreport{bm10:wpn,
  author = {Beffara, Emmanuel and Mogbil, Virgile},
  title = {Concurrent processes as wireless proof nets},
  type = {Technical report},
  number = {hal-00462484},
  note = {Available online at http://hal.archives-ouvertes.fr/hal-00462484/},
  month = feb,
  url = {http://hal.archives-ouvertes.fr/hal-00462484/},
  year = 2010
}

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.

@techreport{bef09:qt,
  author = {Beffara, Emmanuel},
  title = {Quantitative testing semantics for non-interleaving},
  institution = {Institut de Math\'ematiques de Luminy},
  type = {Technical report},
  number = {hal-00397551},
  note = {Available online at http://hal.archives-ouvertes.fr/hal-00397551/},
  month = apr,
  url = {http://hal.archives-ouvertes.fr/hal-00397551/},
  year = 2009
}

This paper presents a logical approach to the translation of functional calculi into concurrent process calculi. The starting point is a type system for the π-calculus closely related to linear logic. Decompositions of intuitionistic and classical logics into this system provide type-preserving translations of the λ- and λμ-calculus, both for call-by-name and call-by-value evaluation strategies. Previously known encodings of the λ-calculus are shown to correspond to particular cases of this logical embedding. The realisability interpretation of types in the π-calculus provides systematic soundness arguments for these translations and allows for the definition of type-safe extensions of functional calculi.

@techreport{bef07:fpp,
  author = {Beffara, Emmanuel},
  title = {Functions as proofs as processes},
  institution = {Institut de Math\'ematiques de Luminy},
  type = {Technical report},
  number = {hal-00609866},
  note = {Available online at http://hal.archives-ouvertes.fr/hal-00609866/},
  month = jan,
  url = {http://hal.archives-ouvertes.fr/hal-00609866/},
  year = 2007
}

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
}