ThEdu'23
ThEdu'23, Programme
Programme — 5 July 2023
| 08:45-09:00 — Welcome & Announcements | |||
09:00–10:00 — Isabelle Proof Assistant in Education - Chair P. Quaresma
| |||
| 09:00–09:30 | Interactive Formal Specification for Mathematical Problems of Engineers | Walther Neuper | presentation |
| 09:30–10:00 | Teaching Higher-Order Logic Using Isabelle | Simon Tobias Lund and Jørgen Villadsen | |
10:00–10:30 — Coffee Break
| |||
10:30–12:30 — Invited Talk & Coq PA in Education - Chair J. Narboux
| |||
| 10:30–11:30 | Invited talk: The challenges of using Type Theory to teach Mathematics | Yves Bertot | |
| 11:30–12:00 | Waterproof: educational software for learning how to write mathematical proofs | Jelle Wemmenhove, Thijs Beurskens, Sean McCarren, Jan Moraal, David Tuin and Jim Portegies | |
| 12:00–12:30 | A Coq Library of Sets for Teaching Denotational Semantics | Qinxiang Cao, Xiwei Wu and Yalun Liang | |
12:30–14:00 — Lunch Break
| |||
14:00–15:30 — PAs in Education & Learning Environments - Chair W. Neuper
| |||
| 14:00–14:30 | Use of two proof assistants in an introduction to proof course: an experiment | Frédéric Tran Minh | |
| 14:30–15:00 | Underlying theories of proof assistants and potential impact on the teaching and learning of proof | Iro Bartzia, Emmanuel Beffara, Antoine Meyer and Julien Narboux | presentation |
| 15:00–15:30 | WebPie: A Tiny Slice of Dependent Types | Christophe Scholliers | |
15:30–16:00 — Coffee Break
| |||
16:00–17:30 — Business Meeting and Closing — Chair Pedro Quaresma
| |||
| 16:00–16:30 | Business Meeting and Closing | Julien Narboux, Walther Neuper and Pedro Quaresma | presentation |
