THEDU — PROGRAM
Days: Sunday, 19 July 2026
Sunday, 19 July 2026
08:30-10:00
ThEdu Session 1
ThEdu
Session Chair:
Location:
C2.01
| 08:30-09:00 |
Complete, Transparent & Interactive Systems for Highschool Mathematics (abstract) 30 min
1 JKU University Linz
|
| 09:00-09:30 |
MiniHOL: A minimal object logic for teaching Isabelle/HOL’s foundations (abstract) 30 min
1 Karlsruhe Institute of Technology
|
| 09:30-10:00 |
CoreCalc: A Core Sequent Calculus Tool (abstract) 30 min
1 Technical University of Denmark
|
10:00-11:00
Coffee Break
ThEdu
Location:
C2.01
11:00-12:00
ThEdu Session 2
ThEdu
Session Chair:
Location:
C2.01
| 11:00-11:30 |
Addressing, with the concourse of CAS, diverse open issues dealing with the manifold and subtle concept of geometric locus (abstract) 30 min
1 Universidad Nebrija
|
| 11:30-12:00 |
Teaching Isabelle to Secondary-School Students: A Case Study (abstract) 30 min
1 None
2 Gymnasium Mariano-Josephinum
|
12:00-14:00
Lunch
ThEdu
Location:
C2.01
14:00-15:30
ThEdu Session 3
ThEdu
Session Chair:
Location:
C2.01
| 14:00-14:30 |
The Educational Proof Assistant Waterproof in an Introductory Proof Course: Proof Construction and Learning Processes (abstract) 30 min
1 Utrecht University
2 Eindhoven University Of Technology
|
| 14:30-15:00 |
Waterproof River: An AI Tutor for Waterproof (abstract) 30 min
1 Radboud University Nijmegen
2 Eindhoven University Of Technology & Utrecht University
3 Eindhoven University Of Technology
|
| 15:00-15:30 |
A Readable Formalization of Propositional Logic in Lean with Yalep (abstract) 30 min
1 IRIF
|
15:30-16:30
Coffee Break
ThEdu
Location:
C2.01
16:30-17:30
ThEdu Session 4
ThEdu
Session Chair:
Location:
C2.01
| 16:30-17:00 |
Isabelle/jEdit — a Generic Frontend for Formal Mathematics (abstract) 30 min
1 JKU University Linz
|
| 17:00-17:30 |
Rocq Game: A Gamified Web-Based Environment for Interactive Learning with a Proof Assistant (abstract) 30 min
1 Technical University of Košice
|