Day 1
TIMES
10:00 - 10:20
10:20 - 10:40
10:40 - 11:00
11:00 - 11:20
11:20 - 11:40
11:40 - 12:00
12:00 - 12:20
12:20 - 12:40
12:40 - 13:00
13:00 - 13:20
13:20 - 13:40
13:40 - 14:00
14:00 - 14:20
14:20 - 14:40
14:40 - 15:00
15:00 - 15:20
15:20 - 15:40
15:40 - 16:00
16:00 - 16:20
16:20 - 16:40
16:40 - 17:00
17:00 - 17:20
Stream 1
Doron Zeilberger
Experimental Mathematics: a Brave new Paradigm
Morning tea
Rajeev Gore
Introduction to Interactive Theorem Proving in Coq
Lunch
Rajeev Gore
Modular Synthesis of Certifying STV Counting Programs
Afternoon tea
Thotsaporn Thanatipanonda
A Probabilistic Two-Pile Game
Daniel Murfet
Proof synthesis and differential linear logic
Day 2
TIMES
10:00 - 10:20
10:20 - 10:40
10:40 - 11:00
11:00 - 11:20
11:20 - 11:40
11:40 - 12:00
12:00 - 12:20
12:20 - 12:40
12:40 - 13:00
13:00 - 13:20
13:20 - 13:40
13:40 - 14:00
14:00 - 14:20
14:20 - 14:40
14:40 - 15:00
15:00 - 15:20
15:20 - 15:40
15:40 - 16:00
16:00 - 16:20
16:20 - 16:40
16:40 - 17:00
17:00 - 17:20
Stream 1
Doron Zeilberger
A case-study in experimental-yet-rigorous mathematics: Analyzing the running time of Quicksort
Morning tea
Robert Y. Lewis
Formalized mathematics in the Lean proof assistant I
Lunch
Robert Y. Lewis
Formalized mathematics in the Lean proof assistant II
Afternoon tea
Alwen Tiu
Specifying and reasoning about operational semantics in the Abella theorem prover
Michael Norrish
Mechanising Computability and Kolmogorov Complexity in HOL
Day 3
TIMES
10:00 - 10:20
10:20 - 10:40
10:40 - 11:00
11:00 - 11:20
11:20 - 11:40
11:40 - 12:00
12:00 - 12:20
12:20 - 12:40
12:40 - 13:00
13:00 - 13:20
13:20 - 13:40
13:40 - 14:00
14:00 - 14:20
14:20 - 14:40
14:40 - 15:00
15:00 - 15:20
Stream 1
Don Taylor
Theorem Proving and Program Development with Magma
Morning tea
Nicole Sutherland
Calculation-Assisted Proof
WiMSIG Lunch
Thotsaporn Thanatipanonda
On average length of Game
Afternoon tea