CIRM Scientific Events
  • CIRM Main website
  • CIRM Visitor information
  • CHAIRE JEAN-MORLET

SLIDES

Effective Analysis: Foundations, Implementations, Certification
January 11 - 15, 2016




  • Andrej Bauer (University of Ljubljana)
Tutorial on Type theory (pdf)
  • Ulrich Berger (Swansea University)
Constructive logic for concurrent real number computation (pdf)
  • Sylvie Boldo (INRIA Saclay)
Formal verification of numerical analysis programs (pdf)
  • Pieter Collins (Maastricht University)
Implementing Logic and Real Arithmetic (pdf)
  • Eva Darulova (Max Planck Institute for Software Systems)
Programming with Numerical Uncertainties (pdf)
  • Boris Djalal (INRIA)
Newton sums for an effective formalization of algebraic numbers (pdf)
  • Fabian Immler (TUM, Germany)
Verified Numerics for ODEs in Isabelle/HOL (pdf)
  • Michal Konečný (Aston University, UK)
Exact Real Number Computation in AERN (pdf) (slides with annotations) (recording)
  • Catherine Lelay (Institute for Advanced Study)
A new approach to formalize real numbers in the UniMath library (pdf)
  • Rob Lewis (Carnegie Mellon University)
Algebra and Analysis in the Lean Theorem Prover (pdf)
  • Victor Magron (Verimag, Grenoble)
Certified Roundoff Error Bounds Using Semidefinite Programming and Formal Floating Point Arithmetic (pdf)
  • Erik Martin-Dorel (Université Paul Sabatier Toulouse)
CoqInterval: A Toolbox for Proving Non-linear Univariate Inequalities in Coq (pdf)
  • Norbert Müller (University of Trier, Germany)
Wrapping in Exact Real Arithmetic (pdf)
  • Iosif Petrakis (University of München)
Bishop's Stone-Weierstrass theorem for compact metric spaces revisited (pdf)
  • Sebastian Posur (Aachen University)
Category theory as a foundation for algorithms and programming in computer algebra (pdf)
  • Egbert Rijke (Carnegie Mellon University)
Localizations at omega-compact types as sequential colimits (pdf) 
  • Monika Seisenberger (Swansea University, UK)
Verification of Discrete and Real-timed Railway Control Systems (pdf)
  • Peter Selinger (Dalhousie University, Canada)
Combining numerical and number-theoretic methods to solve unitary approximation problems in quantum computing (pdf)
  • Bas Spitters (Aarhus University)
Cubical sets as a classifying topos (pdf)
  • Laurent Théry (Inria – Sophia Antipolis Méditerranée)
Proof and Computation in Coq (pdf)

















TRUSTEES 

Picture
Picture
Picture


CIRM - Luminy
​Centre International de Rencontres Mathématiques

163 avenue de Luminy, Case 916
​13288 Marseille cedex 9, FRANCE
​ Tel: +33 (0)4 91 83 30 00​

Download the site map:
Picture

GPS N43°13'48.182'' E5°26'38.46''

Stay connected & informed: