Skip to content

thery/FlocqLecture

Repository files navigation

FlocqLecture

Docker CI

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])

Meta

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

Releases

No releases published

Packages

No packages published