Chair: Tobias Nipkow

• 09:30: Chelsea Edmonds. Lucas's Theorem: Formalising Generating Function Proofs.
• 10:00: Lawrence Paulson. Ackermann's Function in Iterative Form: A Subtle Termination Proof with Isabelle/HOL.
• 10:30: Asta Halkjær From, Jørgen Villadsen. A Concise Sequent Calculus for Teaching First-Order Logic.