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) Peter Schuster (University of Verona) Bas Spitters (Aarhus University) Organizing Committee Assia Mahboubi (Inria Saclay) Speakers
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 |