BPR 
26th June 2017 11:00 to 12:00 
Natarajan Shankar 
The Big Proof Agenda for Mechanizing Mathematical Discourse 

BPR 
27th June 2017 11:00 to 12:00 
Thierry Coquand 
Univalent type theory and modular formalisation of mathematics 

BPR 
27th June 2017 13:30 to 14:30 
Andrew Pitts 
Using Agda to Explore PathOriented Models of Type Theory 

BPR 
28th June 2017 11:00 to 12:00 
MarieFrançoise Roy 
Effectivity and Complexity Results in Hilbert's 17th problem MarieFrançoise Roy Université de Rennes 1, France 

BPR 
29th June 2017 11:00 to 12:00 
Jeremy Avigad 
The Lean Theorem Prover 

BPR 
29th June 2017 15:30 to 17:30 
Andrew Pitts 
HoTT research seminar (Coquand & Rijke) 

BPR 
30th June 2017 10:00 to 11:00 
Natarajan Shankar 
A tutorial introduction to the PVS proof assistant 

BPR 
30th June 2017 11:00 to 12:00 
Andreas Abel 
A tutorial introduction to Agda 

BPR 
3rd July 2017 11:00 to 12:00 
Bas Spitters 
Synthetic topology in Homotopy Type Theory for probabilistic programming 

BPR 
3rd July 2017 15:30 to 16:30 
Johannes Hölzl 
Proof Automation  Automation in Isabelle's Analysis 

BPR 
3rd July 2017 16:30 to 17:30 
Natarajan Shankar 
Inference Algorithms 

BPR 
4th July 2017 10:30 to 11:30 
KuenBang Hou (Favonia) 
Computational HigherDimensional Type Theory 

BPR 
4th July 2017 13:00 to 14:00 
Johannes Hölzl 
Classical Analysis in Lean & Isabelle 

BPR 
4th July 2017 15:30 to 17:30 

Big Proof and Education (coordinated by Jeremy Avigad) 

BPR 
5th July 2017 13:30 to 14:30 
Manuel Eberl 
SemiAutomatic Asymptotics in Isabelle/HOL 

BPR 
5th July 2017 15:30 to 17:30 

Social Proof Seminar (coordinated by Fenner Tanswell) 

BPR 
6th July 2017 11:00 to 12:00 
J Strother Moore 
Industrial Use of a Mechanical Theorem Prover 

BPR 
6th July 2017 13:00 to 13:40 
Chris Kapulkin 
Type theory and higher categories 

BPR 
6th July 2017 13:40 to 14:20 
Fabian Immler 
A Verified ODE Solver and Smale's 14th Problem 

BPR 
6th July 2017 15:30 to 16:30 
Ulrik Buchholtz 
Nominal applications of the classifying space of the finitary permutation group 

BPR 
6th July 2017 16:30 to 17:30 
Martin Hofmann 
Interpretation of the Calculus of Constructions in dictoses 

BPR 
7th July 2017 10:00 to 11:00 
Benedikt Ahrens, Catherine LELAY 
Overview of Unimath 

BPR 
7th July 2017 11:00 to 11:30 
Bas Spitters 
The HoTT library in Coq 

BPR 
7th July 2017 11:30 to 12:00 
Floris van Doorn 
The Lean HoTT library 

BPR 
7th July 2017 12:00 to 12:30 
Dan Licata, KuenBang Hou (Favonia) 
Homotopy Type Theory in Agda 

BPR 
7th July 2017 13:30 to 14:30 
J Strother Moore 
An Industrially Useful Prover 

BPR 
9th July 2017 14:00 to 17:00 
Stephen Watt, Patrick Ion 
International Knowledge Management Trust 

BPRW01 
10th July 2017 10:00 to 11:00 
Thomas Hales 
Big Conjectures 

BPRW01 
10th July 2017 11:30 to 12:30 
Vladimir Voevodsky 
UniMath  its present and its future. 

BPRW01 
10th July 2017 14:30 to 15:30 
Larry Paulson 
Proof Assistants: From Symbolic Logic To Real Mathematics? 

BPRW01 
10th July 2017 16:00 to 17:00 
Stephen Watt 
Mathematical Knowledge at Scale 

BPRW01 
11th July 2017 09:00 to 10:00 
Steve Awodey 
Impredicative encodings in HoTT 

BPRW01 
11th July 2017 10:00 to 11:00 
Martin Escardo 
Logic in univalent type theory 

BPRW01 
11th July 2017 11:30 to 12:30 
Floris van Doorn 
Homotopy Type Theory in Lean 

BPRW01 
11th July 2017 14:30 to 15:30 
Dan Licata 
Small Proofs 

BPRW01 
11th July 2017 16:00 to 17:00 
Peter LeFanu Lumsdaine 
Schemas and semantics for Higher Inductive Types 

BPRW01 
12th July 2017 09:00 to 10:00 
Assia Mahboubi 
Formally Verified Approximations of Definite Integrals 

BPRW01 
12th July 2017 10:00 to 11:00 
Leonardo de Moura 
Metaprogramming with Dependent Type Theory 

BPRW01 
12th July 2017 11:30 to 12:30 
Jasmin Blanchette 
Hammers and Model Finders, and Beyond 

BPRW01 
12th July 2017 14:30 to 15:30 
Ursula Martin 
The social machine of mathematics 

BPRW01 
12th July 2017 16:00 to 17:00 
Marijn Heule 
Everything's Bigger in Texas: ``The Largest Math Proof Ever'' 

BPRW01 
13th July 2017 09:00 to 10:00 
Georges Gonthier 
Scaffolds and frames: the MathComp algebra formal library 

BPRW01 
13th July 2017 10:00 to 11:00 
Tobias Nipkow 
Mining the Archive of Formal Proofs 

BPRW01 
13th July 2017 11:30 to 12:30 
Grant Passmore 
Formal Verification of Financial Algorithms, Progress and Prospects 

BPRW01 
13th July 2017 14:30 to 15:30 
Mateja Jamnik 
Accessible Reasoning with Diagrams: Ontology Debugging 

BPRW01 
13th July 2017 16:00 to 17:00 
Katya Komendenskaya 
Machine Learning for Interactive Theorem Proving: Revisit, Reuse and Recycle your Proofs 

BPRW01 
14th July 2017 09:00 to 10:00 
Alison Pease 
The role of explanation in mathematical research 

BPRW01 
14th July 2017 10:00 to 11:00 
Michael Kohlhase 
Lightweight and Heavyweight Methods for Integrating Mathematical Libraries 

BPRW01 
14th July 2017 11:30 to 12:30 
Jacques Fleuriot 
Proof Archeology: Historical Mathematics from an Interactive Theorem Proving Standpoint 

BPRW01 
14th July 2017 13:30 to 14:30 
Stephanie Dick 
After Math: Reasoning, Computing, and Proof in the Postwar United States (via Skype) 

BPRW01 
14th July 2017 14:30 to 15:30 
William Timothy Gowers, Natarajan Shankar, Patrick Ion 
Panel on future directions for Big Proof 

BPRW01 
14th July 2017 16:00 to 17:00 
William Timothy Gowers, Natarajan Shankar, Patrick Ion 
Panel on future directions for Big Proof 

BPR 
17th July 2017 11:00 to 12:00 
Maria Paola Bonacina 
CDSAT: conflictdriven theory combination 

BPR 
17th July 2017 15:30 to 16:00 
Cesare Tinelli 
SMTCoq, a plugin for the trustworthy integration of SAT/SMT solvers into Coq 

BPR 
17th July 2017 16:00 to 16:30 
Wenda Li 
Evaluating winding numbers through Cauchy indices in Isabelle/HOL 

BPR 
17th July 2017 16:30 to 17:00 
Bohua Zhan 
Auto2 prover in Isabelle 

BPR 
17th July 2017 17:00 to 17:30 
Edward Ayers 
A simple prover in the browser 

BPR 
18th July 2017 11:00 to 12:00 
Paulo Oliva 
Mining Human Proofs from Machine Proofs 

BPR 
18th July 2017 13:30 to 14:30 
Josef Urban 
Combining Machine Learning and Automated Reasoning: Some Training Examples 

BPR 
18th July 2017 15:30 to 16:00 
Fenner Tanswell 
Go forth and multiply! Imperatives in mathematical proofs 

BPR 
18th July 2017 16:00 to 16:30 
Lorenzo Lane 
Socialising proof 

BPR 
18th July 2017 16:30 to 17:30 
Ursula Martin 
Social proof: social session on the POPL experience 

BPR 
21st July 2017 11:00 to 12:00 
James Davenport 
Computer Algebra and Formal Proof 

BPR 
21st July 2017 13:30 to 14:30 
Chris Sangwin 
Reasoning by equivalence: the start of proof in elementary education 

BPR 
24th July 2017 11:00 to 12:00 
Natarajan Shankar, Leonardo de Moura, Arnold Neumaier, Cesare Tinelli 
Language and automation in mathematics 

BPR 
24th July 2017 15:30 to 17:30 
Jeremy Avigad 
Big Proof & Education 

BPR 
25th July 2017 11:00 to 12:00 
Yves Bertot 
Building blocks towards modeling the physical world: analysis, geometry, computer arithmetics 

BPR 
25th July 2017 14:00 to 16:00 
Josef Urban, Mario Carneiro, Bohua Zhan 
Systems Based on Set Theory 

BPR 
26th July 2017 11:00 to 12:00 
Arnold Neumaier 
Concise  a synthesis of types, grammars, semantics 

BPR 
26th July 2017 14:30 to 15:30 
Thomas Hales 
An overview of the Flyspeck project 

BPR 
26th July 2017 15:30 to 16:30 
Joe Corneli 
Modelling the way mathematics is actually done 

BPR 
26th July 2017 16:30 to 17:30 

Social Proof Seminar (coordinated by Fenner Tanswell) 

BPR 
27th July 2017 11:00 to 12:00 
Deepak Kapur 
Parametric Groebner basis computations and elimination 

BPR 
27th July 2017 13:30 to 14:30 
Konstantin Korovin 
Automated theorem proving in firstorder logic: from superposition to instantiation 

BPR 
27th July 2017 15:30 to 16:30 
Vladimir Voevodsky 
Simplicial and cubical sets  how they relate to each other (joint work with Chris Kapulkin) 

BPR 
27th July 2017 16:30 to 17:30 
Benedikt Ahrens 
Categorical structures for type theory in univalent foundations" 

BPR 
28th July 2017 11:00 to 12:00 
Georges Gonthier 
A MathComp Library tour 

BPR 
28th July 2017 13:30 to 14:30 
William Timothy Gowers 
How do human mathematicians avoid big searches? 

BPR 
3rd August 2017 15:30 to 16:30 
Vladimir Voevodsky 
Cubical and simplicial 2  the coherent nerve of a cubical category (joint work with K Kapulkin) 
