Introduction to the Coq proof assistantModelling and verifying algorithms in Coq: an introduction CEA-EDF-INRIA summer school, Paris, 7-11 June 2010. Speakers: Yves Bertot, Pierre Casteran, Pierre Letouzey, Assia Mahboubi. Assistants: Stéphane Glondu, Francesco Zappa Nardelli. The Coq Proof Assistant can be downloaded from here. The files of these lectures have been tested with version 8.2pl1 but should work with any 8.2 (or later) ver
