⚠️ Under construction ⚠️ This website will be officialy launched with the first release of Rocq 9.0 in March 2025.
Until then, there may remain broken links and references to not-yet existing projects.
Inductively Defined Types
Thierry Coquand and Christine Paulin-Mohring, International Conference on Computer Logic: 50-66 — 1988