Sommaire

An Introduction to Programming and Proving with Dependent Types in Coq

Chlipala, Adam

Link
Link


Journal of Formalized Reasoning
An introduction to small scale reflection in Coq

Gonthier, Georges ; Mahboubi, Assia

Link
Link


Journal of Formalized Reasoning
Basic first-order model theory in Mizar

Caminati, Marco Bright

Link
Link


Journal of Formalized Reasoning
Mizar in a Nutshell

Grabowski, Adam ; Kornilowicz, Artur ; Naumowicz, Adam

Link
Link


Journal of Formalized Reasoning