This repo is a fork of the mirror by Miëtek Bak of the Software Foundations series of books.
It seems that the main interest of the mirror is to produce PDF files, while the main interest of this branch on the fork is just tracking changes between releases. Therefore, only sources are contained and change history is compressed.
This table is mostly based on old versions on the official server. The date of the current version is sometimes changed wihtout the version changes. So, it may not reflect actual updates on the server. I can not find lf-6.4 on the server. Dates of lf-6.7 and lf-6.8 are in reversed order as it is.
| 2026/01/09 | 2026/01/07 | 2025/12/27 | 2025/08/24 | 2025/01/06 | 2025/01/13 | 2024/08/25 | 2024/01/03 | 2023/11/29 | 2023/10/10 | 2023/08/27 | 2023/08/23 | 2023/07/06 | 2023/7/6 | 2023/3/25 | 2023/3/23 | 2022/8/28 | 2022/8/8 | 2022/8/1 | 2021/8/11 | 2021/5/26 | |
|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
| 1.Logical Foundations (lf) | 7.0 2026/01/07 13:19 Coq 9.0.0 or later |
6.10.0 2025/12/27 11:45 Coq 9.0.0 or later |
6.9.0 2025/08/24 14:28 Coq 9.0.0 or later |
6.8 2025/01/06 19:47 Coq 8.20 or later |
6.7 2025/01/13 16:01 Coq 8.19.2 or later |
6.6 2024/01/03 15:00 Coq 8.17 or later |
6.5 2023/10/10 11:34 Coq 8.17 or later |
6.3 2023/03/25 11:45 Coq 8.16 or later |
6.2 2022-08-28 10:19 Coq 8.15 or later |
6.1 2022-08-01 17:48 Coq 8.15 or later |
6.0 2021-08-11 15:00, Coq 8.12 or later |
||||||||||
| 2.Programming Language Foundations (plf) | 7.0 2026/01/07 13:35 Coq 9.0.0 or later |
6.10.0 2025/12/27 11:58 Coq 9.0.0 or later |
6.9.0 2025/08/24 14:32 Coq 9.0.0 or later |
6.8 2025/01/06 19:51 Coq 8.20 or later |
6.7 2024/08/25 14:14 Coq 8.17.1 or later |
6.6 2024/01/03 15:07 Coq 8.17 or later |
6.5 2023/08/23 11:33 Coq 8.17 or later |
6.4 2023/07/06 15:52 Coq 8.16 or later |
6.3 2023/03/25 11:47 Coq 8.16 or later |
6.2 2022-08-28 10:22 Coq 8.15 or later |
6.1 2022-08-01 17:52 Coq 8.15 or later |
6.0 2021-05-26 09:59 Coq 8.12 or later |
|||||||||
| 3.Verified Functional Algorithms (vfa) | 2.0 2026/01/07 13:37 Coq 9.0.0 or later |
1.6.0 2025/08/24 14:33 Coq 9.0.0 or later |
1.5.6 2025/01/06 19:53 Coq 8.20 or later |
1.5.5 2024/08/25 14:19 Coq 8.17.1 or later |
1.5.4 2023/08/23 11:35 Coq 8.17 or later |
1.5.3 2023/03/25 11:49 Coq 8.16 or later |
1.5.2 2022-08-29 07:41 Coq 8.15 or later |
1.5.1 2022-08-01 17:56 Coq 8.15 or later |
1.5 2021-05-26 10:02 Coq 8.12 or later |
||||||||||||
| 4.QuickChick: Property-Based Testing in Coq (qc) | 2.0 2026/01/07 13:37 Coq 9.0.0 or later |
1.4.0 2025/08/24 14:33 Coq 9.0.0 or later |
1.3.4 2025/01/06 19:54 Coq 8.20 or later |
1.3.3 2023/08/27 16:23 Coq 8.17 or later |
1.3.2 2023/03/25 11:52 Coq 8.16 or later |
1.3.1 2023-03-25 10:59 Coq 8.16 or later |
1.2.1 2021-08-11 15:19 Coq 8.12 or later |
1.2 2021-05-26 10:04 Coq 8.12 or later |
|||||||||||||
| 5.Verifiable C (vc) | 2.0 2026/01/07 13:39 Rocq 9.0.0 with VST 2.16 |
1.2.2 2023/03/25 11:50 Coq 8.16 with VST 2.10 |
1.2.1 2023/03/23 21:21 Coq 8.16 with VST 2.10 |
1.1.1 2021-08-11 15:23 Coq 8.13 with VST 2.8 |
1.1.0 2021-05-26 10:03 Coq 8.13 with VST 2.7 |
||||||||||||||||
| 6.Separation Logic Foundations (slf) | 3.0 2026/01/07 13:36 Coq 9.0.0 or later |
2.4.0 2025/08/24 14:33 Coq 9.0.0 or later |
2.3 2025/01/06 19:52 Coq 8.20 or later |
2.2 2024/08/25 14:18 Coq 8.17.1 or later |
2.1 2024/01/03 14:54 Coq 8.17 or later |
2.0 2023/11/29 09:28 Coq 8.17 or later |
1.6 2023/08/23 12:59 Coq 8.17 or later |
1.5 2023/07/06 15:47 Coq 8.16 or later |
1.4 2023/03/25 11:51 Coq 8.16 or later |
1.3 2022-08-28 10:27 Coq 8.15 or later |
1.2 2022-08-01 17:59 Coq 8.15 or later |
1.1 2021-08-11 15:27 Coq 8.12 or later |
1.0 2021-05-26 10:04 Coq 8.12 or later |
||||||||
| 7.Security Foundations (secf) | 1.0 2026/01/07 13:38 Rocq 9.0.0 or later |
Maintained by Yak!.