This is an introductory course Floating-Point Numbers and Formal Proof given at ENS Lyon in 2016-2017. It is based on the Flocq Library.
It is composed of four lectures:
Laurent Théry (Laurent.Thery@inria.fr)
- Author(s):
- Laurent Théry
- License: MIT License
- Compatible Coq versions: 8.16 or later
- Additional dependencies:
- Coq namespace:
FlocqLecture
- Related publication(s): none
To build and install manually, do:
git clone https://github.com/thery/FlocqLecture.git
cd FlocqLecture
make # or make -j <number-of-cores-on-your-machine>
make install