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
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
