FlocqLecture
Formal Proof Lecture
An introductory course on floating-point numbers and formal proof using Coq
6 stars
3 watching
1 forks
Language: Coq
last commit: about 2 years ago
Linked from 1 awesome list
coq-formalizationfloating-pointieee-754lecture
Related projects:
| Repository | Description | Stars |
|---|---|---|
 pa-ba/calc-comp | Formalizations of compiler design and virtual machine calculations in Coq | 30 |
 vlopezj/coq-course | A self-reading Coq course for PhD students covering fundamental topics in functional programming and formal verification. | 38 |
 discus-lang/iron | Formalizations of functional languages with a focus on proof and verification | 142 |
| thery/mathcomp-extra | A collection of reusable mathematical components and algorithms implemented in Coq | 5 |
 math-comp/tutorial_material | Tutorials and materials for teaching Coq-based mathematical component development | 17 |
 fblanqui/color | A comprehensive Coq library providing formal definitions and proofs of rewriting theory, lambda-calculus, and termination. | 35 |
 coq-community/fav-ssr | A comprehensive library of verified data structures and algorithms in Coq | 45 |
 xavierleroy/cdf-program-logics | Companion Coq development for teaching program logics | 40 |
| thery/coqprime | A proof assistant library for prime number certification using elliptic curves and Pocklington certificates | 37 |
 dawsonjon/fpu | A synthesizable IEEE 754 floating point library in Verilog. | 538 |
 ilyasergey/pnp | A tutorial project on using Coq to mechanize mathematics with dependent types | 160 |
 mgrabovsky/fm-notes | A collection of notes and resources on formal methods, type theory, and theorem proving using Coq. | 21 |
| xavierleroy/cdf-mech-sem | Development of formal semantics and verification tools for imperative languages and functional programming languages. | 64 |
 reynir/brainfuck | Formalizing Brainfuck in Coq to prove its properties and verify a compiler for simple arithmetic expressions. | 26 |
 charguer/tlc | A Coq library providing an alternative set of axioms and type class mechanisms for building and proving mathematical theorems. | 38 |