Home

Awesome

<!--- This file was generated from `meta.yml`, please do not edit manually. Follow the instructions on https://github.com/coq-community/templates to regenerate. --->

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

Meta

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