Floating-Point Numbers and Formal Proof
An introductory course on formal verification of floating-point numbers and real numbers using the Coq proof assistant and Flocq library.
Overview
FlocqLecture is a structured course that teaches formal verification of floating-point and real numbers using the Coq proof assistant and the Flocq library. It provides hands-on exercises and solutions, making it a practical resource for learning formal methods in numerical computation.
Key Features
- Four Comprehensive Lectures — Covers real numbers, rounding, and formal proofs with step-by-step examples.
- Solution Files Included — Each lecture comes with a solution file for self-checking and deeper understanding.
- Based on Flocq Library — Leverages the widely-used Flocq library for floating-point formalization in Coq.
- Make-Based Build System — Simple installation and building process using standard Make commands.
- Docker Integration — Includes Docker CI workflows for reproducible environments and testing.
Philosophy
FlocqLecture emphasizes practical, hands-on learning by combining theoretical concepts with executable Coq proofs, helping users build confidence in formal verification of numerical algorithms.
Related Projects
Found a gem we're missing?
Open-Awesome is built by the community, for the community. Submit a project, suggest an awesome list, or help improve the catalog on GitHub.
