skip to content
 

Seminars (BPR)

Videos and presentation materials from other INI events are also available.

Search seminar archive

Event When Speaker Title
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 title tba
BPR 29th June 2017
11:00 to 12:00
Jeremy Avigad Metaprogramming in Lean
BPR 29th June 2017
15:30 to 17:30
Andrew Pitts HoTT research seminar (Coquand & Rijke)
BPR 30th June 2017
09:00 to 12:00
Tutorials
BPR 3rd July 2017
11:00 to 12:00
Bas Spitters Synthetic topology in Homotopy Type Theory for probabilistic programming
BPR 5th July 2017
13:00 to 14:00
James Davenport James Davenport
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
09:00 to 10:00
Unimath tutorial
BPR 7th July 2017
13:00 to 14:00
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 tba
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
Ursula Martin The social machine of mathematics
BPRW01 11th July 2017
09:00 to 10:00
Steve Awodey tba
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 tba
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
Marijn Heule Everything's Bigger in Texas: ``The Largest Math Proof Ever''
BPRW01 12th July 2017
16:00 to 17:00
Stephen Watt Mathematical Knowledge at Scale
BPRW01 13th July 2017
09:00 to 10:00
Georges Gonthier tba
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 Tba
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 Proof Mining with Dependent Types
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 tba
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 tba (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 20th July 2017
15:30 to 17:30
Andrew Pitts HoTT research seminar
BPR 27th July 2017
15:30 to 17:30
Andrew Pitts HoTT research seminar
BPR 3rd August 2017
15:30 to 17:30
Andrew Pitts HoTT research seminar
University of Cambridge Research Councils UK
    Clay Mathematics Institute London Mathematical Society NM Rothschild and Sons