Coq 8.4 Reference Manual

Pierre Boutillier (1, 2) , Stephane Glondu (1, 2) , Benjamin Grégoire (3) , Hugo Herbelin (1, 2) , Pierre Letouzey (1, 2) , Pierre-Marie Pédrot (1, 2) , Yann Régis-Gianas (1, 2) , Matthieu Sozeau (1, 2) , Arnaud Spiwack (1) , Enrico Tassi (4, 5)

1 PI.R2 - Design, study and implementation of languages for proofs and programs
2 PPS - Preuves, Programmes et Systèmes
3 MARELLE - Mathematical, Reasoning and Software
4 SPECFUN - Symbolic Special Functions : Fast and Certified
5 MSR - INRIA - Microsoft Research - Inria Joint Centre

Domaines: Langage de programmation [cs.PL]; Logiciel mathématique [cs.MS]; Logique en informatique [cs.LO]

Pierre Boutillier, Stephane Glondu, Benjamin Grégoire, Hugo Herbelin, Pierre Letouzey, et al.. Coq 8.4 Reference Manual. [Research Report] Inria. 2014. ⟨hal-01114602⟩