Introduction to the Coq proof assistant. F. Blanqui. Note. 6 pages, 2013.

These notes have been written for a 7-days school organized at the Institute of Applied Mechanics and Informatics (IAMA) of the Vietnamese Academy of Sciences and Technology (VAST) at Ho Chi Minh City, Vietnam, from Tuesday 12 March 2013 to Tuesday 19 March 2013. The mornings were dedicated to theoretical lectures introducing basic notions in mathematics and logic for the analysis of computer programs. The afternoons were practical sessions introducing the OCaml programming language and the Coq proof assistant (these notes).