CSE-433 Logic in Computer Science - Resources

[ Home | Schedule | Assignments | Software | Resources | Students ] gla@postech Sungwoo Park

Book on Coq

Interactive Theorem Proving and Program Development. Coq'Art: The Calculus of Inductive Constructions. Yves Bertot and Pierre Casteran. Springer.

Documents on Coq

These documents are local copies all obtained from the main Coq homepage.

[ Home | Schedule | Assignments | Software | Resources | Students ] gla@postech Sungwoo Park