Emmanuel Beffara

Research

Themes

My scientific interests include:

  • logical foundations of interactive and non-deterministic systems,
  • linear-algebraic semantics of computation,
  • what happens to the proof/program correspondence outside functional computation,
  • various things related to the above topics,
  • how to teach logic and computer science in middle and high school.

Structures

In the past, I was member of the ANR projects Logoi (Geometry of interaction), Récré (Realizability), Panda (Parallelism and Distribution Analysis), Choco (Curry-Howard and Concurrency) and the PEPS project Quand (Quantitative Approaches to Non-Determinism).

Publications

Journal articles

Order algebras: a quantitative model of interaction
Mathematical Structures in Computer Science, 2017. (HALPDF)
Concurrent nets: a study of prefixing in process calculi
With François Maurel. Theoretical Computer Science, May 2006. (HALPDF)

Conference articles

A proof-theoretic view on scheduling in concurrency
CL&C 2014. (HALPDFslides)
Proofs as executions
With Virgile Mogbil. IFIP TCS, 2012. (HALPDF)
An algebraic process calculus
LICS, 2008. (HALPDF)
A concurrent model for linear logic
MFPS XXI, May 2006. (PDF)
Concurrent nets: a study of prefixing in process calculi
With François Maurel. Express 2004, April 2005. (HALPDF)
Disjunctive normal forms and local exceptions
With Vincent Danos. ICFP 2003. (PDF)
Adapting Gurvich-Karzanov-Khachiyan’s algorithm for parity games: Implementation and experimentation
With Sergei Vorobyov. [Short presentation at LICS’02. (report)
Verification of timed automata using rewrite rules and strategies
With Olivier Bournez, Hassen Kacem, and Claude Kirchner. BISFAI, June 2001. (HAL)

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. (HALPDFdiapos)

Collective works

Situations de recherche pour la classe
IREM de Grenoble, groupe Logique et raisonnement. Deuxième édition, 2017.
Algorithmique et programmation au cycle 4
Groupe Informatique de la CII Lycée. 2017. (PDF)

Thesis

Logique, réalisabilité et concurrence
PhD thesis, 2005. In French. (TELPDF)

Course notes

Introduction to linear logic
August 2013. (HALPDFslides)

Manuscripts

Unifying type systems for mobile processes
April 2015. (HALPDF)
Concurrent processes as wireless proof nets
With Virgile Mogbil. February 2010. (HALPDF)
Quantitative testing semantics for non-interleaving
April 2009. (HALPDF)
Functions as proofs as processes
January 2007. (HALPDF)

Miscellaneous

Realizability with constants
Workshop on Formal Methods and Security, Nanjing, China, 2003. (HALPDF)
Tautologies classiques et combinateurs de contrôle
Master’s thesis, September 2002. (PDF)
Adapting Gurvich-Karzanov-Khachiyan’s algorithm for parity games: Implementation and experimentation
Internship report, August 2001. (PostScript)
Automates temporisés et calcul de réécriture
Internship report, July 2000. (PostScript)