Internal seminar of the SERENA team, Thursday 03 December, 4pm-5pm in building 13: Francois Clément: Safe and Correct Programming for Scientific Computing
Abstract: The increasing complexity of algorithms for modern scientific computing makes it a major challenge to implement them in the traditional imperative languages that are popular in the community. The idea is to explore the usage of formal tools from computing science, and in particular from the functional programming school, to design and implement generic tools that may ease the development of scientific computing software. In this lecture, we will focus on:
- Sklml, an easy coarse grain parallelization compiler system;
- Ref-indic, a generic inversion platform for adaptive parameter estimation;
- a comprehensive mechanical proof of correctness of a C program as a PDE solver.
Basic examples of the use of OCaml, Sklml, and Coq will be given.
