The picture "Le coq mécanisé" is courtesy of Lilia Anisimova

Programs and Proofs: Mechanizing Mathematics with Dependent Types

Ilya Sergey, IMDEA Software Institute

JetBrains/SPbSU Summer School — 25-29 August 2014

              

This summer school offers a brief and practically-oriented introduction to the basic concepts of mechanized reasoning and interactive theorem proving using the Coq proof assistant.

The primary audience of the lectures are the students with expertise in software development and programming and knowledge of discrete mathematic disciplines on the level of an undergraduate university program. The high-level goal of the course is, therefore, to demonstrate how much the rigorous mathematical reasoning and development of robust and intellectually manageable programs have in common, and how understanding of common programming language concepts provides a solid background for building mathematical abstractions and proving theorems formally. The low-level goal of this course is to provide an overview of the Coq proof assistant, taken in its both incarnations: as an expressive functional programming language with dependent types and as a proof assistant providing support for mechanized interactive theorem proving.

By aiming these two goals, this school is, thus, intended to provide a demonstration how the concepts familiar from the mainstream programming languages and serving as parts of good programming practices can provide illuminating insights about the nature of reasoning in Coq's logical foundations and make it possible to reduce the burden of mechanical theorem proving. These insights will eventually give the student a freedom to focus solely on the essential part of the formal development instead of fighting with the proof assistant in futile attempts to encode the "obvious" mathematical intuition.


Course materials

Lectures

Title Coq file Additional materials Solutions for exercises
1 Introduction N/A
Introduction - Slides (PDF)
Formally Verified Mathematics, by Jeremy Avigad and John Harrison
Meet the Engineer (video)
Hari Seldon (Wikipedia article)
N/A
2 Functional Programming in Coq FunProg.v
GNU Emacs Reference Card
There and Back Again by Olivier Danvy and Mayer Goldberg
FunProg_solutions.v
3 Propositional Logic LogicPrimer.v
Proofs and Types by Jean-Yves Girard
LogicPrimer_solutions.v
4 Equality and Rewriting Principles Rewriting.v Rewriting_solutions.v
5 Views and Boolean Reflection BoolRefl.v BoolReflect_solutions.v
6 Inductive Reasoning in SSReflect SsrStyle.v
Pigeonhole principle (Wikipedia article)
Frobenius problem (Wikipedia article)
SsrStyle_solutions.v
7 Encoding Mathematical Structures DepRecords.v
Generic Proof Tools And Finite Group Theory (François Garillot's PhD Thesis)
Typeclassopedia by Brent Yorgey
DepRecords_solutions.v
8 Case Study: Program Verification in Hoare Type Theory HTT.v
Verification in HTT - Slides (PDF)
Structuring the Verification of Heap-Manipulating Programs by Aleks Nanevski et al.
Languages as Libraries by Sam Tobin-Hochstadt et al.
The manuscripts of Edsger W. Dijkstra
HTT_solutions.v

Further reading

Books and courses on Coq and its applications

Research papers


Pictures of the participants


Last modified: Wed Dec 9 01:43:50 +08 2020