Please note that the program is not yet finalized and details may be subject to change.
Aarhus Summer School on Programming Languages, Logic, and Software Security
August 10–14, 2026 ・ Aarhus University
Mon, Aug 10th | Tue, Aug 11th | Wed, Aug 12th | Thu, Aug 13th | Fri, Aug | |
| 9:00-10:30 | Rocq | Rocq | HO-SL | TT | LBS |
| 10:30-11:00 | Break | Break | Break | Break | Break |
| 11:00-12:30 | Rocq | Rocq | HO-SL | LBS | HO-SL |
| 12:30-13:30 | Lunch | Lunch | Lunch | Lunch | Lunch |
| 13:30-15:00 | TT | TT | TT | HO-SL | HO-SL |
| 15:00-15:30 | Break | Break | Break | Break | Break |
| 15:30-17:00 | LBS | LBS | TT | HO-SL | Dinner & concert at Tivoli Friheden |
| Abbr. | Course | Speaker |
| Rocq | The Rocq Proof Assistant and Generative AI Tools for Formalisation of Mathematics | Bas Spitters |
| HO-SL | Higher-Order Concurrent Separation Logic | Lars Birkedal & Amin Timany |
| TT | Introduction to Type Theory | Daniel Gratzer |
| LBS | Language-Based Security | Aslan Askarov |
Each session is 1.5 hours. Breaks of 30 minutes are scheduled between morning sessions and between afternoon sessions. Lunch break is 12:30–13:30. Friday evening is reserved for a joint social activity.
The Rocq course (Mon–Tue) provides foundational skills in interactive theorem proving and is closely related to the courses on Higher-Order Concurrent Separation Logic and Introduction to Type Theory, which begin on Wednesday and Monday afternoon, respectively.
