see also the index (by topic, by tool, by reference, by year)
Coq
The Coq proof assistant
- Accurate discriminant
- Approximated Cosine in C annotated in ACSL
- Approximated Cosine in Why3
- Approximated Cosine, exact values and rounding errors
- Area of a triangle
- Binary Heaps in Why3
- Defining Bernoulli and Binomial distributions from flip
- Discretization of the 1D acoustic wave equation
- Exact subtraction: Sterbenz's theorem
- Fibonacci sequence, linear algorithm, Java version
- Filter elements of an array
- Linear recurrence of order 2
- Malcolm algorithm to determine the radix
- Sparse Arrays in Capucine
- Termination of a random walk
- WP revisited in Why3
see also the index (by topic, by tool, by reference, by year)