skip to content
 

Seminars (BPR)

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

Search seminar archive

Event When Speaker Title Presentation Material
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
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 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)
University of Cambridge Research Councils UK
    Clay Mathematics Institute London Mathematical Society NM Rothschild and Sons