MPCTT Textbook Project

Modeling and Proving in Computational Type Theory Using the Rocq Prover
Gert Smolka

pdf
Rocq