Skip to Main Content
Mobile Menu

B: Computer-Aided Proofs

(Organized by Sam Buss and Vijay Ganesh)

Session B1: Monday, March 20 in EDUC 109

10:30 – 11:10 Oliver Kullmann (Swansea University), Solving mathematical problems with SAT
11:20 – 12:00 Nikolaj Bjørner (Microsoft Research), From models to proofs and back in automated theorem proving

Session B2: Wednesday, March 22 in EDUC 109

10:30 – 11:10 Georges Gonthier (Inria), Big proofs, little math
11:20 – 12:00 Floris van Doorn (Carnegie Mellon University), Eilenberg-Maclane spaces in homotopy type theory