|
BPR |
18th July 2017 |
Ursula Martin |
Social proof: social session on the POPL experience |
|
|
BPR |
18th July 2017 |
Lorenzo Lane |
Socialising proof |
|
|
SIN |
18th July 2017 |
Andrew Duncan |
Measuring Sample Discrepancy with Diffusions |
 |
|
BPR |
18th July 2017 |
Fenner Tanswell |
Go forth and multiply! Imperatives in mathematical proofs |
|
|
SIN |
18th July 2017 |
Anthony Maggs |
Multi-scale algorithms for simple fluids |
|
|
BPR |
18th July 2017 |
Josef Urban |
Combining Machine Learning and Automated Reasoning: Some Training Examples |
|
|
SIN |
18th July 2017 |
Michela Ottobre |
Sampling with non-reversible dynamics |
|
|
SIN |
18th July 2017 |
Michel Manon |
Event-chain algorithms: taming randomness in Monte Carlo methods through irreversibility, factorization and lifting |
|
|
SIN |
18th July 2017 |
Robert Jack |
How does breaking detailed balance accelerate convergence to equilibrium? |
|
|
BPR |
18th July 2017 |
Paulo Oliva |
Mining Human Proofs from Machine Proofs |
|
|
SIN |
18th July 2017 |
Joris Bierkens |
Piecewise deterministic Markov processes and efficiency gains through exact subsampling for MCMC |
|
|
BPR |
17th July 2017 |
Edward Ayers |
A simple prover in the browser |
|
|
BPR |
17th July 2017 |
Bohua Zhan |
Auto2 prover in Isabelle |
|
|
BPR |
17th July 2017 |
Wenda Li |
Evaluating winding numbers through Cauchy indices in Isabelle/HOL |
 |
|
BPR |
17th July 2017 |
Cesare Tinelli |
SMTCoq, a plug-in for the trustworthy integration of SAT/SMT solvers into Coq |
|
|
BPR |
17th July 2017 |
Maria Paola Bonacina |
CDSAT: conflict-driven theory combination |
|
|
BPRW01 |
14th July 2017 |
William Timothy Gowers, Natarajan Shankar, Patrick Ion |
Panel on future directions for Big Proof |
|
|
BPRW01 |
14th July 2017 |
William Timothy Gowers, Natarajan Shankar, Patrick Ion |
Panel on future directions for Big Proof |
|
|
BPRW01 |
14th July 2017 |
Stephanie Dick |
After Math: Reasoning, Computing, and Proof in the Postwar United States (via Skype) |
|
|
BPRW01 |
14th July 2017 |
Jacques Fleuriot |
Proof Archeology: Historical Mathematics from an Interactive Theorem Proving Standpoint |
|
|
BPRW01 |
14th July 2017 |
Michael Kohlhase |
Lightweight and Heavyweight Methods for Integrating Mathematical Libraries |
|
|
BPRW01 |
14th July 2017 |
Alison Pease |
The role of explanation in mathematical research |
|
|
BPRW01 |
13th July 2017 |
Katya Komendenskaya |
Machine Learning for Interactive Theorem Proving: Revisit, Reuse and Recycle your Proofs |
|
|
BPRW01 |
13th July 2017 |
Mateja Jamnik |
Accessible Reasoning with Diagrams: Ontology Debugging |
|
|
BPRW01 |
13th July 2017 |
Grant Passmore |
Formal Verification of Financial Algorithms, Progress and Prospects |
|
|
BPRW01 |
13th July 2017 |
Tobias Nipkow |
Mining the Archive of Formal Proofs |
|
|
BPRW01 |
13th July 2017 |
Georges Gonthier |
Scaffolds and frames: the MathComp algebra formal library |
|
|
BPRW01 |
12th July 2017 |
Marijn Heule |
Everything's Bigger in Texas: ``The Largest Math Proof Ever'' |
|
|
BPRW01 |
12th July 2017 |
Ursula Martin |
The social machine of mathematics |
|
|
BPRW01 |
12th July 2017 |
Jasmin Blanchette |
Hammers and Model Finders, and Beyond |
|
|
BPRW01 |
12th July 2017 |
Leonardo de Moura |
Metaprogramming with Dependent Type Theory |
|
|
BPRW01 |
12th July 2017 |
Assia Mahboubi |
Formally Verified Approximations of Definite Integrals |
|
|
BPRW01 |
11th July 2017 |
Peter LeFanu Lumsdaine |
Schemas and semantics for Higher Inductive Types |
|
|
BPRW01 |
11th July 2017 |
Dan Licata |
Small Proofs |
|
|
BPRW01 |
11th July 2017 |
Floris van Doorn |
Homotopy Type Theory in Lean |
|
|
BPRW01 |
11th July 2017 |
Martin Escardo |
Logic in univalent type theory |
|
|
BPRW01 |
11th July 2017 |
Steve Awodey |
Impredicative encodings in HoTT |
|
|
BPRW01 |
10th July 2017 |
Stephen Watt |
Mathematical Knowledge at Scale |
|
|
BPRW01 |
10th July 2017 |
Larry Paulson |
Proof Assistants: From Symbolic Logic To Real Mathematics? |
 |
|
BPRW01 |
10th July 2017 |
Vladimir Voevodsky |
UniMath - its present and its future. |
|
|
BPRW01 |
10th July 2017 |
Thomas Hales |
Big Conjectures |
|
|
BPR |
9th July 2017 |
Stephen Watt, Patrick Ion |
International Knowledge Management Trust |
|
|
BPR |
7th July 2017 |
J Strother Moore |
An Industrially Useful Prover |
|
|
BPR |
7th July 2017 |
Dan Licata, Kuen-Bang Hou (Favonia) |
Homotopy Type Theory in Agda |
|
