SLIDES – NOTES

Analyse effective: fondations, programmation, certification
11 au 15 janvier 2016

Tutorial on Type theory (pdf)

Constructive logic for concurrent real number computation (pdf)

Formal verification of numerical analysis programs (pdf)

Implementing Logic and Real Arithmetic (pdf)

Programming with Numerical Uncertainties (pdf)

  • Boris Djalal (INRIA)

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

Verified Numerics for ODEs in Isabelle/HOL (pdf)

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

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

Algebra and Analysis in the Lean Theorem Prover (pdf)

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

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

Wrapping in Exact Real Arithmetic (pdf)

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

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

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

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

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

Cubical sets as a classifying topos (pdf)

Proof and Computation in Coq (pdf)