Emmanuel Beffara
33
Documents
Présentation
Je suis [maître de conférences ](http://www.enseignementsup-recherche.gouv.fr/cid22657/maitres-de-conferences.html)à l'[Université Grenoble Alpes](http://www.univ-grenoble-alpes.fr/) et au[ Laboratoire d'informatique de Grenoble](http://www.liglab.fr/).
Recherche
---------
Je suis membre de l'équipe [MeTAH](https://metah.imag.fr/) du [LIG](http://www.liglab.fr/). Mes centres d'intérêt scientifiques incluent:
- la didactique de l’informatique et de la logique
- la correspondance preuves/programmes et ses prolongements et applications
### Projets
- [ANR](https://anr.fr/) Asmodée, Analyse et conception de situations de médiation en informatique débranchée (2022–2024)
- [Pégase](https://www.polepilote-pegase.fr/), Pôle pilote de formation des enseignants et de recherche pour l’éducation (2021–2031)
- [STIC-Amsud](https://www.sticmathamsud.org/) APCoRe, An algebrization program for concurrent realizability (2022–2023)
Enseignement
------------
Ça se passe dans le cadre de l'[Inspé](https://inspe.univ-grenoble-alpes.fr/), principalement en master[ MEEF](http://formations.univ-grenoble-alpes.fr/fr/catalogue/master-XB/arts-lettres-langues-ALL/master-meef-second-degre-program-master-meef-second-degre.html) (métiers de l'enseignement de l'éducation et de la formation) second degré, dans les parcours [Numérique et sciences informatiques ](http://formations.univ-grenoble-alpes.fr/fr/catalogue/master-XB/arts-lettres-langues-ALL/master-meef-second-degre-program-master-meef-second-degre/parcours-numerique-et-sciences-informatiques-1re-annee-subprogram-parcours-numerique-et-sciences-informatiques.html)et [Mathématiques](http://formations.univ-grenoble-alpes.fr/fr/catalogue/master-XB/arts-lettres-langues-ALL/master-meef-second-degre-program-master-meef-second-degre/parcours-mathematiques-subprogram-parcours-mathematiques.html).
Autres
------
À venir…
Publications
Jeux combinatoires et pensée informatiqueTangente Éducation, 2020
Article dans une revue
hal-03291745v1
|
|
|
Une analyse des exercices d’algorithmique et de programmation du brevet 2017Repères IREM, 2019, 116, pp.47-81
Article dans une revue
hal-02077738v2
|
|
Order algebras: a quantitative model of interactionMathematical Structures in Computer Science, 2018, ⟨10.1017/S0960129516000360⟩
Article dans une revue
hal-00429610v3
|
Concurrent nets: a study of prefixing in process calculiTheoretical Computer Science, 2006, 356 (3), pp.356-373. ⟨10.1016/j.tcs.2006.02.009⟩
Article dans une revue
hal-00151817v1
|
|
Vers une cartographie des Situations d'Informatique débranchéeColloque Didapro 10 sur la Didactique de l’informatique et des STIC, 2024, Louvain-La-Neuve, Belgique. pp.99-107
Communication dans un congrès
hal-04482116v2
|
Modélisation des connaissances mobilisées dans une situation de généralisation de motifColloque Didapro 10 sur la Didactique de l’informatique et des STIC, 2024, Louvain-La-Neuve, Belgique. pp.159-159
Communication dans un congrès
hal-04485409v1
|
|
Underlying theories of proof assistants and potential impact on the teaching and learning of proof12th International Workshop on Theorem proving components for Educational software, Julien Narboux; Walther Neuper; Pedro Quaresma, Jul 2023, Rome, Italy
Communication dans un congrès
hal-04227823v1
|
|
|
Instrumentation de l'association de registres sémiotiques dans un assistant de preuveEIAH2023 - 11ème Conférence sur les Environnements Informatiques pour l'Apprentissage Humain, Association des Technologies de l’Information pour l’Éducation et la Formation, Jun 2023, Brest, France. pp.1-5
Communication dans un congrès
hal-04096240v1
|
|
Concurrent Realizability on Conjunctive StructuresFSCD 2023 - 8th International Conference on Formal Structures for Computation and Deduction, Jul 2023, Rome, Italy
Communication dans un congrès
hal-04083002v2
|
|
Les abstractions informatiques peuvent-elles concrétiser les mathématiques?Séminaire de didactique des mathématiques 2018, Nov 2018, Paris, France
Communication dans un congrès
hal-02535820v1
|
|
A proof-theoretic view on scheduling in concurrencyClassical Logic and Computation 2014, Jul 2014, Wien, Austria. pp.78-92, ⟨10.4204/EPTCS.164.6⟩
Communication dans un congrès
hal-00951976v4
|
|
Proofs as Executions7th International Conference on Theoretical Computer Science (TCS), Sep 2012, Amsterdam, Netherlands. pp.280-294, ⟨10.1007/978-3-642-33475-7_20⟩
Communication dans un congrès
hal-00586459v2
|
An algebraic process calculusLogic in Computer Science, Jun 2008, Pittsburgh, United States. pp.130--141
Communication dans un congrès
hal-00397531v1
|
|
A concurrent model for linear logic2006, pp.147-168, ⟨10.1016/j.entcs.2005.11.055⟩
Communication dans un congrès
hal-00151820v1
|
|
Concurrent nets: a study of prefixing in process calculi2004, pp.67-86, ⟨10.1016/j.entcs.2004.11.029⟩
Communication dans un congrès
hal-00009192v1
|
|
Disjunctive normal forms and local exceptions2003, pp.203-211, ⟨10.1145/944705.944724⟩
Communication dans un congrès
hal-00009191v1
|
|
Verification of Timed Automata Using Rewrite Rules and StrategiesERCIM Working Group on Constraints, Jun 2001, Prague, Czech Republic, 15 p
Communication dans un congrès
inria-00100534v1
|
|
Verification of Timed Automata Using Rewrite Rules and StrategiesThe Seventh Biennal Bar-Ilan Symposium on the Foundations of Artificial Intelligence - BISFAI'01, Jun 2001, Bar-Ilan University, Ramat-Gan, Israel, 15 p
Communication dans un congrès
inria-00100535v1
|
Programmes, preuves et fonctions : le ménage à trois de Curry-HowardPhilippe Langlois. Informatique mathématique : Une photographie en 2013, Presses Universitaires de Perpignan, 2013, 978-2-35412-183-9
Chapitre d'ouvrage
hal-03652486v1
|
|
L’algorithme : pourquoi et comment le définir pour l'enseigner2023
Pré-publication, Document de travail
hal-04112182v1
|
|
Proof assistants for undergraduate mathematics education: elements of an a priori analysis2023
Pré-publication, Document de travail
hal-04087080v1
|
Concurrent Realizability on Conjunctive Structures2022
Pré-publication, Document de travail
hal-03710542v1
|
|
|
Une analyse de la notion de booléen et de son usage dans l'enseignement de la programmation2022
Pré-publication, Document de travail
hal-03812698v1
|
|
Unifying type systems for mobile processes2015
Pré-publication, Document de travail
hal-01144215v1
|
|
Concurrent processes as wireless proof nets2010
Pré-publication, Document de travail
hal-00462484v1
|
|
Quantitative testing semantics for non-interleaving2009
Pré-publication, Document de travail
hal-00397551v1
|
|
Realizability with constants2003
Pré-publication, Document de travail
hal-00003724v1
|
|
Une analyse des exercices d'algorithmique et de programmation des DNBCommission inter-IREM informatique. 2023
Rapport
hal-03996891v2
|
|
Algorithmique et programmation au cycle 4CII Lycée. 2017
Rapport
hal-03961063v1
|
|
Functions as proofs as processes2007
Rapport
hal-00609866v1
|
|
Logique, Réalisabilité et ConcurrenceMathématiques [math]. Université Paris-Diderot - Paris VII, 2005. Français. ⟨NNT : ⟩
Thèse
tel-00011205v1
|
|
Introduction to linear logicMaster. Italy. 2013
Cours
cel-01144229v1
|