Morning session
| 9:00-9:45 | Dan Synek
An Odyssey of Proof Assistants |
| 10:00-10:45 | Josef Urban
Hol(y)Hammer: An Online ATP service for HOL Light |
| 11:00-11:45 | Mark AdamsTactician. |
Afternoon session
| 14:00-14:45 | Tran Nam TrungHypermaps |
| 15:00-15:45 | Hoang Le TruongFlyspeck: Main estimate |
| 16:00-16:45 | Tom HalesWhat’s left in Flyspeck. |