MPCTT
MPCTT Textbook Project
Modeling and Proving in Computational Type Theory Using the Rocq Prover
Gert Smolka
pdf
Rocq