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:

1. Real numbers (solution)
2. Rounding (solution)
3. Proof I (solution)
4. Proof II (solution)

Laurent Théry ([email protected])

• Author(s):
  • Laurent Théry
• License: MIT License
• Compatible Coq versions: 8.16 or later
• Additional dependencies:
  • Flocq 4.1 or later
• 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