Effective Analysis: Foundations, Implementations, Certification
January 11 – 15, 2016
Effective analysis is the foundation of both symbolic and numerical algorithms which compute properties of continuous objects and of their implementation in mathematical software.

This workshop aims to bring together researchers from different areas, interested in effective methods in analysis and geometry, and by the design and implementation of efficient and certified algorithms. Its objective is to stimulate discussions between communities that do not so often meet in traditional venues and to foster interactions between their different but complementary perspectives, in the tradition of the meetings of the MAP community.

It will address perspectives from proof theory, type theory, constructive analysis, machine-checked mathematics, implementation of real/float/interval arithmetic, computer algebra systems, including those based on new paradigms like quantum computation.

Scientific Committee

Thierry Coquand (University of Gothenburg)
Assia Mahboubi (Inria Saclay)
Marie-Françoise Roy (Université Rennes 1)

Peter Schuster (University of Verona)
Bas Spitters (
Aarhus University)

Organizing Committee

Assia Mahboubi (Inria Saclay)
Peter Schuster (
University of Verona)
Bas Spitters (Aarhus University)


Tutorial on Type theory

Constructive logic for concurrent real number computation

Formal verification of numerical analysis programs

Implementing Logic and Real Arithmetic

Programming with Numerical Uncertainties

  • Boris Djalal (INRIA)

Newton sums for an effective formalization of algebraic numbers

Verified Numerics for ODEs in Isabelle/HOL

Exact Real Number Computation in AERN

A new approach to formalize real numbers in the UniMath library

Algebra and Analysis in the Lean Theorem Prover

Towards a constructive theory of O-minimal structures

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

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

Wrapping in Exact Real Arithmetic

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

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

Localizations at omega-compact types as sequential colimits

Verification of Discrete and Real-timed \\ Railway Control Systems

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

Cubical sets as a classifying topos

Proof and Computation

Basins of attraction for optimal third-order multiple-root finders