Emmanuel Beffara - Publications

Journal articles

Order algebras: a quantitative model of interaction

July 2011. To appear in Mathematical Structures in Computer Science. detailsHALPDF ]

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 https://hal.archives-ouvertes.fr/hal-00429610/},
  month = jul,
  url = {https://hal.archives-ouvertes.fr/hal-00429610/},
  year = 2011
}

Concurrent nets: a study of prefixing in process calculi

With François Maurel. Theoretical Computer Science, May 2006. detailsHALPDF ]

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,
		url = {https://hal.archives-ouvertes.fr/hal-00009192v1}
}

Conference papers

A proof-theoretic view on scheduling in concurrency

CL&C 2014. detailsHALPDFslides ]

This paper elaborates on a new approach of the question of the proof-theoretic study of concurrent interaction called "proofs as schedules". Observing that proof theory is well suited to the description of confluent systems while concurrency has non-determinism as a fundamental feature, we develop a correspondence where proofs provide what is needed to make concurrent systems confluent, namely scheduling. In our logical system, processes and schedulers appear explicitly as proofs in different fragments of the proof language and cut elimination between them does correspond to execution of a concurrent system. This separation of roles suggests new insights for the denotational semantics of processes and new methods for the translation of π-calculi into prefix-less formalisms (like solos) as the operational counterpart of translations between proof systems.

@inproceedings{bef14:scheduling,
  author = {Beffara, Emmanuel},
  title = {A proof-theoretic view on scheduling in concurrency},
  booktitle = {Classical Logic and Computation 2014},
  pages = {78-92},
  series = {Electronic Proceedings in Theoretical Computer Science},
  volume = 164,
  year = 2014,
  doi = {10.4204/EPTCS.164.6},
  url = {https://hal.archives-ouvertes.fr/hal-00951976},
}

Proofs as executions

With Virgile Mogbil. IFIP TCS, 2012. detailsHALPDF ]

This paper proposes a new interpretation of the logical contents of programs in the context of concurrent interaction, wherein proofs correspond to valid executions of a processes. A type system based on linear logic is used, in which a given process has many 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 interaction scenario. A completeness result is established, stating that every lock-avoiding execution of a process in some environment corresponds to a particular typing. Besides traces, types contain precise information about the flow of control between a process and its environment, and proofs are interpreted as composable schedulings of processes. In this interpretation, logic appears as a way of making explicit the flow of causality between interacting processes.

@inproceedings{bm12:pae,
  author = {Beffara, Emmanuel and Mogbil, Virgile},
  title = {Proofs as executions},
  booktitle = {{IFIP} {TCS}},
  pages = {280-294},
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  volume = 7604,
  year = 2012
}

An algebraic process calculus

LICS, 2008. detailsHALPDF ]

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
}

A concurrent model for linear logic

MFPS XXI, May 2006. detailsPDF ]

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
}

Concurrent nets: a study of prefixing in process calculi

With François Maurel. Express 2004, April 2005. detailsHALPDF ]

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
}

Disjunctive normal forms and local exceptions

With Vincent Danos. ICFP 2003. detailsPDF ]

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
}

Adapting Gurvich-Karzanov-Khachiyan's algorithm for parity games:
Implementation and experimentation

With Sergei Vorobyov. Short presentation at LICS'02. detailsreport ]

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

Verification of timed automata using rewrite rules and strategies

With Olivier Bournez, Hassen Kacem, and Claude Kirchner. BISFAI, June 2001. detailsHAL ]

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
}

Book chapter

Programmes, preuves et fonctions: le ménage à trois de Curry-Howard

With Lionel Vaux. In Informatique Mathématique: une photographie en 2013. In French. detailsHALPDFdiapos ]
@inbook{bv13:menage,
  author = {Beffara, Emmanuel and Vaux, Lionel},
  editor = {Langlois, Philippe},
  title = {Informatique Math\'ematique: une photographie en 2013},
  chapter = {Programmes, preuves et fonctions : le m\'enage \`a trois de Curry-Howard},
  publisher = {PUP},
  year = 2013
}

Thesis

Logique, réalisabilité et concurrence

PhD thesis, 2005. In French. detailsTELPDF ]

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
}

Course notes

Introduction to linear logic

August 2013. detailsHALPDFslides ]

This manuscript is the lecture notes for the course of the same title I gave at the Summer school on linear logic and geometry of interaction that took place in Torino in August 2013. The aim of this course is to give a broad introduction to linear logic, covering enough ground to present many of the ideas and techniques of the field, while staying at a (hopefully) accessible level for beginners. For this reason, most technical development is carried out in the simple multiplicative fragment, with only hints at generalizations. As prerequisites, some knowledge of classical sequent calculus and some knowledge of the &lam;-calculus is useful.

@techreport{bef13:intro-ll,
  author = {Beffara, Emmanuel},
  title = {Introduction to linear logic},
  type = {Lecture notes},
  month = aug,
  url = {https://hal.archives-ouvertes.fr/cel-01144229/}
  year = 2013
}

Manuscripts

Unifying type systems for mobile processes

April 2015. detailsHALPDF ]

We present a unifying framework for type systems for process calculi. The core of the system provides an accurate correspondence between essentially functional processes and linear logic proofs; fragments of this system correspond to previously known connections between proofs and processes. We show how the addition of extra logical axioms can widen the class of typeable processes in exchange for the loss of some computational properties like lock-freeness or termination, allowing us to see various well studied systems (like i/o types, linearity, control) as instances of a general pattern. This suggests unified methods for extending existing type systems with new features while staying in a well structured environment and constitutes a step towards the study of denotational semantics of processes using proof-theoretical methods.

@techreport{bef15:unifying,
  author = {Beffara, Emmanuel},
  title = {Unifying type systems for mobile processes},
  type = {Technical report},
  number = {hal-01144215},
  note = {Available online at https://hal.archives-ouvertes.fr/hal-01144215/},
  month = apr,
  url = {https://hal.archives-ouvertes.fr/hal-01144215/},
  year = 2015
}

Concurrent processes as wireless proof nets

With Virgile Mogbil. February 2010. detailsHALPDF ]

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 https://hal.archives-ouvertes.fr/hal-00462484/},
  month = feb,
  url = {https://hal.archives-ouvertes.fr/hal-00462484/},
  year = 2010
}

Quantitative testing semantics for non-interleaving

April 2009. detailsHALPDF ]

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 https://hal.archives-ouvertes.fr/hal-00397551/},
  month = apr,
  url = {https://hal.archives-ouvertes.fr/hal-00397551/},
  year = 2009
}

Functions as proofs as processes

January 2007. detailsHALPDF ]

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 https://hal.archives-ouvertes.fr/hal-00609866/},
  month = jan,
  url = {https://hal.archives-ouvertes.fr/hal-00609866/},
  year = 2007
}

Miscellaneous

Realizability with constants

Workshop on Formal Methods and Security, Nanjing, China, 2003. detailsHALPDF ]

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

Tautologies classiques et combinateurs de contrôle

Master's thesis, September 2002. detailsPDF ]

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
}

Adapting Gurvich-Karzanov-Khachiyan's algorithm for parity games:
Implementation and experimentation

Internship report, August 2001. detailsPostScript ]
@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
}

Automates temporisés et calcul de réécriture

Internship report, July 2000. detailsPostScript ]

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
}