• Andrej Bauer (University of Ljubljana)

Tutorial on Type theory (pdf)

• Ulrich Berger (Swansea University)

Constructive logic for concurrent real number computation (pdf)

• Sylvie Boldo (INRIA Saclay)

Formal verification of numerical analysis programs (pdf)

• Pieter Collins (Maastricht University)

Implementing Logic and Real Arithmetic (pdf)

• Eva Darulova (Max Planck Institute for Software Systems)

Programming with Numerical Uncertainties (pdf)

• Boris Djalal (INRIA)

Newton sums for an effective formalization of algebraic numbers (pdf)

• Fabian Immler (TUM, Germany)

Verified Numerics for ODEs in Isabelle/HOL (pdf)

• Michal Konečný (Aston University, UK)

Exact Real Number Computation in AERN (pdf) (slides with annotations) (recording)

• Catherine Lelay (Institute for Advanced Study)

A new approach to formalize real numbers in the UniMath library (pdf)

• Rob Lewis (Carnegie Mellon University)

Algebra and Analysis in the Lean Theorem Prover (pdf)

• Victor Magron (Verimag, Grenoble)

Certified Roundoff Error Bounds Using Semidefinite Programming and Formal Floating Point Arithmetic (pdf)

• Erik Martin-Dorel (Université Paul Sabatier Toulouse)

CoqInterval: A Toolbox for Proving Non-linear Univariate Inequalities in Coq (pdf)

• Norbert Müller (University of Trier, Germany)

Wrapping in Exact Real Arithmetic (pdf)

• Iosif Petrakis (University of München)

Bishop’s Stone-Weierstrass theorem for compact metric spaces revisited (pdf)

• Sebastian Posur (Aachen University)

Category theory as a foundation for algorithms and programming in computer algebra (pdf)

• Egbert Rijke (Carnegie Mellon University)

Localizations at omega-compact types as sequential colimits (pdf) 

• Monika Seisenberger (Swansea University, UK)

Verification of Discrete and Real-timed Railway Control Systems (pdf)

• Peter Selinger (Dalhousie University, Canada)

Combining numerical and number-theoretic methods to solve unitary approximation problems in quantum computing (pdf)

• Bas Spitters (Aarhus University)

Cubical sets as a classifying topos (pdf)

• Laurent Théry (Inria – Sophia Antipolis Méditerranée)

Proof and Computation in Coq (pdf)