Research
Themes
My scientific interests include:
- didactics of logic and computer science
- logical foundations of interactive and non-deterministic systems
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 - QCOMICAL
-
Quantum Computing and Its Calculi
MSCA Staff Exchanges, 2024–2028, led by Benoît Valiron and Alejandro Díaz-Caro
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
- Faustine Oliva, Des programmes qui prouvent : étude de la signification des démonstrations assistées par ordinateur pour la connaissance mathématique (started in 2022), supervised with Gabriella Crocco
- Luigi Bernardi, Logic Education: Playing with True and False (2020-2024), supervised with Myriam Quatrini and Lorenzo Tortora de Falco
- Michele Alberti, On operational properties of quantitative extensions of λ-calculus (2011–2014), supervised with Lionel Vaux and Ugo Dal Lago
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. (HAL – PDF)
- 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. (HAL – PDF)
- Les abstractions informatiques peuvent-elles concrétiser les mathématiques ?
- EB. Actes du Séminaire de didactique des mathématiques 2018. (HAL – PDF)
- A proof-theoretic view on scheduling in concurrency
- EB. CL&C 2014. (HAL – PDF – slides)
- Proofs as executions
- EB, Virgile Mogbil. IFIP TCS, 2012. (HAL – PDF)
- An algebraic process calculus
- EB. LICS, 2008. (HAL – PDF)
- Concurrent nets: a study of prefixing in process calculi
- EB, François Maurel. Theoretical Computer Science, May 2006. (HAL – PDF)
- A concurrent model for linear logic
- EB. MFPS XXI, May 2006. (HAL – PDF)
- Concurrent nets: a study of prefixing in process calculi
- EB, François Maurel. Express 2004, April 2005. (HAL – PDF)
- Disjunctive normal forms and local exceptions
- EB, Vincent Danos. ICFP 2003. (AHL – PDF)
- 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. (HAL – arXiv)
- Unifying type systems for mobile processes
- EB. April 2015. (HAL – PDF)
- Concurrent processes as wireless proof nets
- EB, Virgile Mogbil. February 2010. (HAL – PDF)
- Quantitative testing semantics for non-interleaving
- EB. April 2009. (HAL – PDF)
- Functions as proofs as processes
- EB. January 2007. (HAL – PDF)
- Realizability with constants
- EB. Workshop on Formal Methods and Security, Nanjing, China, 2003. (HAL – PDF)
- 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. (HAL – PDF – slides)
- Programmes, preuves et fonctions: le ménage à trois de Curry-Howard
- EB, Lionel Vaux. Book chapter, in Informatique Mathématique: une photographie en 2013. (HAL – PDF – diapos)
- Logique, réalisabilité et concurrence
- EB. PhD thesis, 2005. In French. (TEL – PDF)