CONFERENCE
Analyse effective: fondations, programmation, certification
11 au 15 janvier 2016
L’analyse effective est le cadre formel qui permet d’étudier les algorithmes aussi bien symboliques que numériques établissant des propriétés d’objets continus, ainsi que leurs implantations dans les logiciels de calcul scientifique. Cette rencontre a pour but de rassembler des chercheurs d’horizons variés, intéressés par les méthodes effectives en analyse et géométrie, et par la conception et l’implantation d’algorithmes efficaces et certifiés. Il s’agit d’encourager les discussions entre membres de communautés qui ont rarement l’occasion de se rencontrer dans les conférences plus spécialisées, et de stimuler les interactions entre leurs perspectives différentes mais complémentaires, dans la traditions des rencontres de la communauté MAP. Les exposés invités proposeront des perspectives issues de la théorie de la démonstration, de la théorie des types, de l’analyse constructive, des mathématiques formalisées, de l’arithmétique flottante, ainsi que des systèmes de calcul formels, incluant un système basé sur le paradigme du calcul quantique.

Comité scientifique

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)

Comité d’organisation

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

Conférenciers 

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