09:00
10:00
11:00
12:00
13:00
14:00
15:00
16:00
17:00
18:00
19:00
20:00
21:00
22:00
›9:00 (1h)
Mechanical and User-friendly Lemmas for Lagrange finite elements and floating-point Errors in Rocq
Sylvie Boldo
Sylvie Boldo
› D8 001
9:00 - 10:00 (1h)
Mechanical and User-friendly Lemmas for Lagrange finite elements and floating-point Errors in Rocq
D8 001
Sylvie Boldo
https://raim2025.sciencesconf.org/data/program/slides_sylvie_boldo.pdf›10:00 (30min)
› D8 001
10:00 - 10:30 (30min)
Optimal Quantization of Rank-One Matrices in Floating-Point Arithmetic
D8 001
Elisa Riccietti
10:30 - 11:00 (30min)
Coffee break
D8 004
11:00 - 12:00 (1h)
Learning about Computer Arithmetic by Formally Verifying It
D8 001
John Harrison
12:00 - 14:00 (2h)
Lunch
D8 004
14:00 - 15:00 (1h)
Elementary Functions (or not) ... and Implementation
D8 001
Florent de Dinechin
›15:00 (30min)
› D8 001
15:00 - 15:30 (30min)
Computer Arithmetic on the 8-bit Floating-Point Formats G.711 alaw and ulaw
D8 001
Christoph Lauter
15:30 - 16:00 (30min)
Coffee break
D8 004
16:00 - 17:00 (1h)
Rounding Error Statistics as Numerics Signature
D8 001
Peter Tang
19:30 - 22:30 (3h)
Dinner at PY restaurant (16, Cours Vitton 69006 Lyon)
