CoqInTheClassroom
This page collects material related to Coq teaching or using Coq and related interfaces as a support for teaching.
We are also starting a wiki page to try to get a more exhaustive list of Universities teaching Coq.
From 1993, the TYPES summer school had courses on Coq as part of its curriculum. In particular, Yves Bertot's course in 2006 led to a tutorial named Coq in a hurry. Notice that other proof assistants related to the TYPES European working group were taught too (in the 2007 edition, this included Isabelle, Matita and Mizar). Most attendees were PhD students but these summer schools were opened to senior people too.
Between 1999 and 2002, a few formations were organised by the TypiCal team (formerly Coq team). It was generally three-day-long intensive formations hosting senior people from industry and academy. The material is now rather old as the last such session was using Coq V7.2.
In 2006, Pierre Castéran proposed a 3-hours introduction to Coq at the JFLA conference. It was based on his formalisation of ordinals and entitled Le Coq au Pauillac et aux omégas.
In 2006, Adam Chlipala and George Necula taught Interactive Computer Theorem Proving at Berkeley university, focusing on Coq and Twelf.
The University of Pennsylvania Provers Group ran a 2008 POPL tutorial, Using Proof Assistants for Programming Language Research. Extensively documented Coq code, illustrating type soundness for simply typed lambda calculus and system F-sub, is available from the website.
An Asian-Pacific summer school was held in 2009, 2010, 2011, 2012 and 2013 (part of material here).
A school on Modelling and verifying algorithms in Coq was held in 2010 in Paris.
A spring school on the Formalization of Mathematics was held in Nice-Sophia-Antipolis in 2012.
A short course on the formalization of mathematics at the initial school of the IHP 2014 special trimester.
A winter school on Software verification and computer proof in Nice in 2014.
A spring school on Mechanizing proofs of programs (archive) was held in 2015 in Fréjus (France).
A short tutorial was given in Nanjing as part of ITP 2015.
Coq is regularly taught as part of the Oregon Programming Languages Summer School.
A number of Coq-based short courses on verified software systems were included in the DeepSpec Summer School in July, 2017.
A former experience of using Coq as a teaching tool and not just per is by Jean Goubault-Larrecq at ENSTA in 1999 (a course on software safety). The Course notes (in French) are available on the teacher's page.
Another experiment has been made by David Delahaye, Mathieu Jaume and Virgile Prevosto to teach semantics of programming languages and software safety at the master-level of CNAM, a university for adults. The paper Ref1 (in French) describes this experience.
A similar master-level class on formal methods and specification languages has been taught by Catherine Dubois using Coq. This was at ENSIIE (archive), a computer science engineer school attached to the CNAM. Groups were composed of 15 to 20 students.
In 2004, Pierre Castéran and Richard Moot used Coq in the context of a course on Proof automation for type-logical grammars] at ESSLLI. Their Coq material is avalaible online.
In 2007, Yves Bertot used Coq as a support for an intensive 4-day class Semantics in Calculus of Constructions at Chalmers University. The course notes are freely available.
Amy Felty used Coq as a tool for a class on Principles of Formal Software Development Fall 2007 (archive) at Ottawa University.
Benjamin Pierce, Stephanie Weirich, and Steve Zdancewic use Coq as a tool for teaching Software Foundations at the University of Pennsylvania (notes used also at Portland State Portland, Maryland, Lehigh, Iowa, USCD, Purdue, Aarhus, ...).
Andrew W. Appel used Coq in a class on Automated Theorem Proving Fall 2007 at Princeton University. This moved to a Programming Languages class using the Software Foundations material.
Paweł Urzyczyn used Coq as a tool for teaching Theoretical Foundations of Theorem Proving Systems (Winter 2006-07) at Warsaw University.
Greg Morrisett (Harvard): I've been teaching an undergraduate PL course using Coq. We've done a big chunk of Winskell's book, and parts of Pierce's book as well. The course website is here.
Yves Bertot (INRIA): For teaching purpose, I have a project on the thorough description of a very small imperative programming language. The development contains two variants of operational semantics (small-step --also called SOS in my development-- or big-step --also called natural semantics), denotational semantics, Hoare logic, Dijkstra's weakest precondition calculus, and abstract interpretation; I intended to add a formally verified compiler. The programming language I work on is minimal, as it only contains constructs for assignment, while-loops and sequences and each aspect is covered in a few hundred lines of Coq code.
For teaching Logic, Pierre Castéran used Coq for long. His material (in French) is publicly available.
In 2003, Frédérique Guilhot formalised geometry in a way close to the way it is teached in French high schools. A dedicated extension GeoView of PCoq was designed in the same time. It seems that the conclusion was that much work was necessary before submitting such tools to high school pupils. The paper Ref2 (in French) describes this experience and the corresponding formalisation of geometry is available as a Coq user contribution which can also serve as the base axiomatic for Julien Narboux' GeoProof.
From 2004, Loïc Pottier and André Hirschowitz started using Coq for teaching mathematics to undergraduate students at the University of Nice. They set up a Wiki Coq Web that collects course notes and exercises, all of them being formally checkable via a Coq web server. The Coq web server, CoqWeb, can also be used via the Wims collection of exercises. See the description at the PATE'07 workshop.
In 2005, Cezary Kaliszyk developed ProofWeb, a web server that allows to use online Coq and other proof assistants. This service has been used as a tool for various classes in computer science and mathematics at the University of Nijmegen (see paper Ref3).
In 2006 and 2007, Aaron Stump used Coq as a tool to teach Logic and Discrete Math at the undergraduate level. One of the objective was to learn students what a proof is.
In 2007, Jakub Sakowicz and Jacek Chrząszcz developed Papuq, an extension of CoqIde designed for teaching logic and set theory at Warsaw University (see paper Ref5).
In 2007, Sungwoo Park started to teach a logic class using Coq for the assignments at Postech.
In 2008, Anne Mulhern taught an informal semester long seminar CoqTalks on using Coq to write formal proofs and using the Penn PL club metatheory library to prove language properties.
Coq is used in a master class on geometry at the university of Strasbourg.
A thread on using Coq for teaching on the Coq-Club mailing list.
The TYPES Proof Assistants and Types in Education (PATE 2007) workshop.
The GeoProof user interface for formal proofs in geometry.
Ref1: D. Delahaye, M. Jaume, V. Prevosto, Coq, un outil pour l'enseignement, Technique et Science Informatiques, vol. 24(9), Langages applicatifs, pp 1139-1160, Hermes Science, 2005.
Ref2: F. Guilhot, Formalisation en Coq et visualisation d'un cours de géométrie pour le lycée, Technique et Science Informatiques, vol. 24(9), Langages applicatifs, pp 1113-1138, Hermes Science, 2005.
Ref3: Kaliszyk, F. Wiedijk, Teaching logic using a state-of-the-art proof assistant, Proceedings of PATE'07, H. Geuvers and P. Courtieu editors. Elsevier, 2007.
Ref4: Narboux, Toward the use of a proof assistant to teach mathematics, Proceedings of ICTMT7, 2005.
Ref5: Sakowicz, J. Chrząszcz, Papuq, a Coq assistant, Proceedings of PATE'07, H. Geuvers and P. Courtieu editors. Elsevier, pp 79-96, 2007.
To the extent possible under law, the contributors of “Cocorico!, the Coq wiki” have waived all copyright and related or neighboring rights to their contributions.
By contributing to Cocorico!, the Coq wiki, you agree that you hold the copyright and you agree to license your contribution under the CC0 license or you agree that you have permission to distribute your contribution under the CC0 license.