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

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, Fondements interactifs de la logique et apprentissage du raisonnement (started in 2020), 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)
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: 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

Une analyse des exercices d’algorithmique et de programmation des DNB: Commission inter-IREM Informatique, 2023. (HAL)
Une analyse de la notion de booléen et de son usage dans l’enseignement de la programmation: Commission inter-IREM Informatique, 2022. (HAL)
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)

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)