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) Comité d’organisation Assia Mahboubi (INRIA Saclay) 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
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 |