Preliminary Program

All the talks and demos will take place in Amphi B at ENS Lyon.

Wednesday, September 3

10:00 am - 10:30 am
 Welcome, registration and coffee
10:30 am - 11:00 am
 Welcome and Opening Remarks
11:00 am - 12:00 am
 Invited Talk 1
P. Markstein: A Fast Quad Precision Elementary Function Library for Itanium
12:00 am - 2:00 pm
 Lunch Break
2:00 pm - 3:30 pm Session 1
  • V. Brattka: Plottable real number functions
  • W. Hu and Q. Zhou: Almost Decidable Predicates of Real Variables
  • M. Ziegler: Stability versus Speed in a Computable Algebraic Model
3:30 pm - 4:00 pm
 Coffee Break
4:00 pm - 5:30 pm
 Session 2
  • H. Bronnimann and G. Melquiond: The Boost interval arithmetic library
  • D. Bailey and X. Li: A comparison of three high-precision quadrature schemes
  • L. Fousse and P. Zimmermann: Accurate summation: towards a simpler and formal proof


Thursday, September 4

9:30 am - 10:30 am
 Invited Talk 2
B. Mourrain: ROXANE: Reliable Open Software-Components for Algebraic and Numeric Efficiency
10:30 am - 10:45 am
 Coffee Break
10:45 am - 12:00 am
 Software Demos
  • C. Daramy: Crlibm: a correctly rounded elementary function library.
  • J. Detrey: FPLibrary: operators for the design of real number processing cores on FPGA
  • N. Mueller: iRRAM: exact real arithmetic in C++
  • N. Revol: MPFI: a library for arbitrary precision interval arithmetic
12:00 am - 1:15 pm
 Lunch Break
2:00 pm - 4:00 pm
 Guided tour of Lyon
6:00 pm - 7:00 pm
 Welcome Reception at City Hall
8:00 pm
 Conference Banquet


Friday, September 5

9:30 am - 10:30 am
 Invited Talk 3
J. Harrison: Formal Verification of Mathematical Algorithms
10:30 am - 11:00 am
 Coffee Break
11:00 am - 12:00 am
 Session 3
  • V. Lefèvre: Multiplication by an Integer Constant: Lower Bounds on the Code Length
  • P. Kornerup and J.-M. Muller: Choosing starting values for certain Newton-Raphson Iterations
12:00 am - 2:00 pm
 Lunch Break
2:00 pm - 3:30 pm
 Session 4
  • I. Takeuti: Effective Limit in Computable Analysis
  • M. Parker: Three concepts of decidability for subsets of uncountable spaces
  • K. Tadaki: Upper bound by Kolmogorov complexity for the probability in computable quantum measurement
3:30 pm - 4:00 pm
 Coffee Break
4:00 pm - 5:30 pm
 Session 5
  • J.-M. Chesneaux, L.-S. Didier and F. Rico: Fixed CADNA library
  • S. Graillat and P. Langlois: Testing polynomial primality with pseudozeros
  • R. Avot-Chotin, J.-M. Chesneaux and J.-L. Lamotte: On the computation of the CESTAC function