ThEdu'24
ThEdu'24, Programme
Programme
| |||
|---|---|---|---|
July 1 | |||
| Session 1 | Chair: Jeremy Avigad | ||
| 16:30 | Proof assistants for teaching: a survey | Frédéric Tran Minh, Laure Gonnord and Julien Narboux | abstract |
| 17:00 | A Web-Based Interactive Tutorial Environment for Isabelle | Nadine Karsten and Kim Jana Eiken | abstract |
| 17:30 | Teaching Divisibility and Binomials with Coq | Sylvie Boldo, Francois Clement, David Hamelin, Micaela Mayero and Pierre Rousselin | abstract |
July 2 | |||
| Session 2 | Chair: Walther Neuper | ||
| 9:00 | Proofs-as-programs for programmers | Jean-Francois Monin and Pierre Corbineau | abstract |
| 9:30 | Investigating students’ activity when using the Natural Number Game | Athina Thoma, Paola Iannone and Gihan Marasingha | abstract |
| 10:00 | Using a proof assistant in an introduction to proof course: first experiment with two proof assistants | Evmorfia-Iro Bartzia, Pierre Boutry and Julien Narboux | abstract |
| Session 3 | Chair: Pedro Quaresma | ||
| 11:00 | Invited Talk: Teaching with Lean | Jeremy Avigad | |
| 12:00 | Maths with Coq in L1 | Pierre Rousselin, Micaela Mayero and Marie Kerjean | abstract |
| Session 4 | Chair: Julien Narboux | ||
| 14:00 | Framed typing | Julien Puydt | abstract |
| 14:30 | Exploratory study of subsets in type theory for Waterproof | Jelle Wemmenhove, Paul van der Horst and Jim Portegies | abstract |
| 15:00 | A graphical interface for category theory proofs in Coq | Luc Chabassier | abstract |
| 15:30 | Minimal Sequent Calculus for Teaching First-Order Logic: Lessons Learned | Jørgen Villadsen | abstract |
| Session 5 | Chair: Jørgen Villadsen | ||
| 16:30 | OnlineProver: First Experience with Teaching Formal Proofs | Joachim Tilsted Kristensen, Ján Perháč, Lars Tveito, Lars-Bo Husted Vadgaard, Michael Kirkedal Thomsen, Oleks Shturmov, Samuel Novotný, Sergej Chodarev and William Steingartner | abstract |
| 17:00 | GNU Aris: a web application for students | Saksham
Attri, Zoltán Kovács and Aaron Windischbauer | abstract |
| 17:30 | On automated completion of geometry statements and proofs with GeoGebra Discovery | Zoltán Kovács, Tomas Recio and M. Pilar Velez | abstract |
| 18:00 | Business meeting | ||
List of Accepted Papers
- GNU Aris: a web application for students,Saksham Attri, Zoltán Kovács and Aaron Windischbauer,abstract
- A graphical interface for category theory proofs in Coq,Luc Chabassier,abstract
- A Web-Based Interactive Tutorial Environment for Isabelle,Nadine Karsten and Kim Jana Eiken, abstract
- Minimal Sequent Calculus for Teaching First-Order Logic: Lessons Learned, Jørgen Villadsen, abstract
- Framed typing,Julien Puydt,abstract
- Using a proof assistant in an introduction to proof course: first experiment with two proof assistants,Evmorfia-Iro Bartzia, Pierre Boutry and Julien Narboux,abstract
- Proofs-as-programs for programmers, Jean-Francois Monin and Pierre Corbineau,abstract
- Teaching Divisibility and Binomials with Coq,Sylvie Boldo, Francois Clement, David Hamelin, Micaela Mayero and Pierre Rousselin,abstract
- The Deaduction project,Frederic Le Roux,abstract
- Exploratory study of subsets in type theory for Waterproof,Jelle Wemmenhove, Paul van der Horst and Jim Portegies, abstract
- Maths with Coq in L1, Pierre Rousselin, Micaela Mayero and Marie Kerjean,abstract
- Investigating students’ activity when using the Natural Number Game,Athina Thoma, Paola Iannone and Gihan Marasingha,abstract
- Proof assistants for teaching: a survey, Frédéric Tran Minh, Laure Gonnord and Julien Narboux, abstract
- OnlineProver: First Experience with Teaching Formal Proofs, Joachim Tilsted Kristensen, Ján Perháč, Lars Tveito, Lars-Bo Husted Vadgaard, Michael Kirkedal Thomsen, Oleks Shturmov, Samuel Novotný, Sergej Chodarev and William Steingartner, abstract
- On automated completion of geometry statements and proofs with GeoGebra Discovery, Zoltán Kovács, Tomas Recio and M. Pilar Velez, abstract
