Prosa
Definitions and proofs for real-time system schedulability analysis.
- from
- Coq
- added
- 2026-10-10
- likes
- 0
similar
-
Coquelicot gitlab.inria.fr
Formalization of classical real analysis compatible with the standard library and focusing on usability.
-
CoqInterval gitlab.inria.fr
Tactics for performing proofs of inequalities on expressions of real numbers.
-
Program verification with types and logic gitlab.science.ru.nl
Lectures and exercise material for a course in programming language semantics, type systems and program logics, using Coq, at Radboud University Nijmegen.
-
Programs and Proofs ilyasergey.net
Book that gives a brief and practically-oriented introduction to interactive proofs in Coq which emphasizes the computational nature of inductive reasoning about decidable propositions via a small set of primitives from the SSReflect proof language.
-
Formal Reasoning About Programs adam.chlipala.net
Book that simultaneously provides a general introduction to formal logical reasoning about the correctness of programs and to using Coq for this purpose.
-
Proofs and Types paultaylor.eu
Jean-Yves Girard.
Coq › Projects > Verified Software: “Definitions and proofs for real-time system schedulability analysis.”