|
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 Path-Oriented Models of Type Theory |
|
|
BPR |
28th June 2017
11:00 to 12:00 |
Marie-Françoise Roy |
Effectivity and Complexity Results in Hilbert's 17th problem Marie-Franç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 |
Kuen-Bang Hou (Favonia) |
Computational Higher-Dimensional 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 |
Semi-Automatic 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, Kuen-Bang 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: conflict-driven theory combination |
|
|
BPR |
17th July 2017
15:30 to 16:00 |
Cesare Tinelli |
SMTCoq, a plug-in 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 |
Joseph 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 first-order 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) |
|
