Emmanuel Beffara

Research

Themes

My scientific interests include:

Structures

I am a member of the team MeTAH of the LIG laboratory in Grenoble. I am involved in the following projects:

Pégase
Pôle pilote de formation des enseignants et de recherche pour l’éducation
PIA3, 2021–2031, led by Jérôme Clerc
Asmodée
Analyse et conception de situations de médiation en informatique débranchée
ANR, 2022–2024, led by Éric Duchêne and Aline Parreau
APCoRE
An Algebrization Program for Concurrent Realizability
STIC-AmSud, 2022–2024, led with Mauro Jaskelioff, Laurent Regnier and Alberto Pardo

In 2021–2022, I was the holder of the IRGA project DISemiDé (Didactique en informatique semi-débranchée).

From 2007 to 2020, I was a member of the team Logique de la programmation of the I2M laboratory in Marseille. I have been a 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).

Students

Theses

Publications

Work in progress

Proof assistants for undergraduate mathematics education: elements of an a priori analysis
Evmorfia-Iro Bartzia, EB, Antoine Meyer and Julien Narboux. April 2023. (HAL)
L’algorithme : pourquoi et comment le définir pour l’enseigner
EB. École de printemps Demimes. April 2023. (HAL)
Towards a fully complete game model for first order classical logic
EB, Luigi Bernardi and Lorenzo Tortora de Falco. February 2023.

Published works

Modélisation des connaissances mobilisées dans une situation de généralisation de motif
Gaëlle Walgenwitz, Marie-Caroline Croset, EB. Didapro 10. (HAL)
Vers une cartographie des Situations d’Informatique débranchée
Julian Lecocq Mage, Simon Modeste, EB, Eric Duchene, Aline Parreau, Maryna Rafalska. Didapro 10. (HAL)
Un jeu de plateau pour comprendre la dualité en logique
EB, Martin Bodin. Adjectif, 2024. (online)
Underlying theories of proof assistants and potential impact on the teaching and learning of proof
Evmorfia-Iro Bartzia, EB, Antoine Meyer and Julien Narboux. ThEdu’23. (HAL)
Concurrent realizability on conjunctive structures
EB, Félix Castro, Mauricio Guillermo and Étienne Miquey. FSCD 2023. (HAL)
Instrumentation de l’association de registres sémiotiques dans un assistant de preuve
EB, Martin Bodin, Rémi Molinier and Nadine Mandran. Poster at EIAH 2023. (HAL)
Jeux combinatoires et pensée informatique
EB. Tangente éducation 55, December 2020. (HALPDF)
Une analyse des exercices d’algorithmique et de programmation du brevet 2017
Commission inter-IREM Informatique. Repères-IREM 116, 2019. (HAL)
Order algebras: a quantitative model of interaction
EB. Mathematical Structures in Computer Science, 2018. (HALPDF)
Les abstractions informatiques peuvent-elles concrétiser les mathématiques ?
EB. Actes du Séminaire de didactique des mathématiques 2018. (HALPDF)
A proof-theoretic view on scheduling in concurrency
EB. CL&C 2014. (HALPDFslides)
Proofs as executions
EB, Virgile Mogbil. IFIP TCS, 2012. (HALPDF)
An algebraic process calculus
EB. LICS, 2008. (HALPDF)
Concurrent nets: a study of prefixing in process calculi
EB, François Maurel. Theoretical Computer Science, May 2006. (HALPDF)
A concurrent model for linear logic
EB. MFPS XXI, May 2006. (HALPDF)
Concurrent nets: a study of prefixing in process calculi
EB, François Maurel. Express 2004, April 2005. (HALPDF)
Disjunctive normal forms and local exceptions
EB, Vincent Danos. ICFP 2003. (AHLPDF)
Adapting Gurvich-Karzanov-Khachiyan’s algorithm for parity games: Implementation and experimentation
EB, Sergei Vorobyov. Short presentation at LICS’02. (report)
Verification of timed automata using rewrite rules and strategies
EB, Olivier Bournez, Hassen Kacem, and Claude Kirchner. BISFAI, June 2001. (HAL)

Collective works

Booléens en programmation : une analyse à destination des enseignants
Commission inter-IREM Informatique. Radix, 2024. (HAL)
Une analyse des exercices d’algorithmique et de programmation du brevet 2017
Commission inter-IREM Informatique. Repères IREM, 2019. (HAL, extended version)
Situations de recherche pour la classe
Groupe Logique et raisonnement. Brochure de l’IREM de Grenoble, 2017. (PDF)
Algorithmique et programmation au cycle 4
Groupe Informatique de la CII Lycée. Brochure IREM, 2017. (PDF)

Manuscripts

Concurrent realizability on conjunctive structures
EB, Félix Castro and Mauricio Guillermo. December 2021. (HALarXiv)
Unifying type systems for mobile processes
EB. April 2015. (HALPDF)
Concurrent processes as wireless proof nets
EB, Virgile Mogbil. February 2010. (HALPDF)
Quantitative testing semantics for non-interleaving
EB. April 2009. (HALPDF)
Functions as proofs as processes
EB. January 2007. (HALPDF)
Realizability with constants
EB. Workshop on Formal Methods and Security, Nanjing, China, 2003. (HALPDF)
Tautologies classiques et combinateurs de contrôle
EB. Master’s thesis, September 2002. (PDF)
Adapting Gurvich-Karzanov-Khachiyan’s algorithm for parity games: Implementation and experimentation
EB. Internship report, August 2001. (PostScript)
Automates temporisés et calcul de réécriture
EB. Internship report, July 2000. (PostScript)

Miscellaneous

Introduction to linear logic
EB. Lecture notes, August 2013. (HALPDFslides)
Programmes, preuves et fonctions: le ménage à trois de Curry-Howard
EB, Lionel Vaux. Book chapter, in Informatique Mathématique: une photographie en 2013. (HALPDFdiapos)
Logique, réalisabilité et concurrence
EB. PhD thesis, 2005. In French. (TELPDF)