FlocqLecture

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 (Laurent.Thery@inria.fr)

Meta

• 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

Building and installation instructions

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