Floating-Point Numbers and Formal Proof

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.