A Formalization of Core Why3 in Coq

on YouTube ↗18m

" summary

Formalization of Why3's core logic as a machine-checked denotational semantics in Coq maps Why3 types to Coq sets, builds explicit encodings for recursive features (algebraic data types via W-types for ADTs, inductive predicates via impredicative encodings, recursive functions via well‑founded recursion), and constructs a correct‑by‑construction natural deduction proof system plus tactics. The development proves consistency, constructs models for well‑typed definitions, verifies parts of Why3's standard library (lists, trees) and proves soundness of two real transformations (let elimination and axiomatization of inductive predicates) with reusable artifacts available.

AI-written summary · about

" chapters (12)

1. 0:00Deductive verifiers and Why3
2. 1:44Verifying tool chains
3. 2:45Foundational verification
4. 3:46Automation with guarantees
5. 4:51Why3 in pipelines
6. 6:36Why3 recursive structures
7. 7:39Denotational semantics in Coq
8. 9:03Recursive structures in Coq
9. 10:51Verifying Why3 transformations
10. 12:17Proof system and tactics
11. 13:19Summary and future work
12. 14:24Q&A