TIMETABLE
All times are Canberra time (AEDT, UTC +11).
Lectures will be held in Room S1 3.07 in the Science Teaching Building (136 Linnaeus Way).
Week 1 (1-5 December)
| Mon | Tue | Wed | Thu | Fri | |
| 08:50 | Opening | ||||
| 09:00 - 10:00 |
Fundamentals of Metalogic (John Slaney) |
Introduction to Interactive Theorem-Proving with Isabelle (Liam O'Connor) |
|||
| 10:20 - 11:20 | Fundamentals of Metalogic | Introduction to Interactive Theorem-Proving with Isabelle | |||
| 11:40 - 12:40 | Fundamentals of Metalogic |
Computability and Incompleteness (Michael Norrish) |
|||
| BREAK | |||||
| 14:00 - 15:00 |
Overview of Automated Reasoning (Peter Baumgartner) |
Computability and Incompleteness | |||
| 15:20 - 16:20 | Overview of Automated Reasoning | Introduction to Interactive Theorem-Proving with Isabelle | |||
Week 2 (8-12) December
| Mon | Tue | Wed | Thu | Fri | |
|---|---|---|---|---|---|
| 09:00 - 10:00 |
Intuitionistic Modal Logic
(Sonia Marin) |
||||
| 10:20 - 11:20 |
Advanced Isabelle for Software Verification
(Chelsea Edmonds) |
||||
| 11:40 - 12:40 |
Resolution for Modal Logics and its Implementation
(Cláudia Nalon) |
||||
| BREAK | |||||
| 14:00 - 15:00 |
Barriers to Entailment
(Gillian Russell) |
||||
| 15:20 - 16:20 |
Modal Type Theories and Logical Relations (Vineet Rajani) |
||||