SLIDES – NOTES
11 au 15 janvier 2016
- 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)