Documentación disponible
en el sitio web de COQ (RECOMENDADO!)Este curso se desarrolla también para la Licenciatura en Ciencias de la Computación de la FCEIA, UNR (Argentina)
Documentación disponible
en el sitio web de COQ (RECOMENDADO!)The
Coq Proof AssistantCoq
Tutorial,
Tutorial on Recursive Types in Coq The
Coq'Art, the first book dedicated to the Coq proof assistant
(Yves
Bertot, Pierre Casteran)Z.
Luo. Computation and Reasoning: A Type Theory for Computer Science,
volume
11 of International Series of Monographs on Computer Science. Oxford
Science
Publications, 1994.F.
Monin. Comprendre les méthodes Formelles. Masson, 1996.C.
Paulin-Mohring and B. Werner. Synthesis of ML programs in the system
Coq.
Journal of Symbolic Computation, (15):607-640, 1993.S.
Thompson. Type Theory and Funtional Programming. Addison-Wesley, 1991.Formal
Methods Specification and Verification Guidebook for Software and
Computer
Systems. Volume I: Planning and Technology Insertion.
NASA-GB-002-95
Release 1.0 . July (formato pdf) 95.