Programs and Proofs

Mechanizing Mathematics with Dependent Types

Lecture notes with exercises

Ilya Sergey

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

These lecture notes are the result of the author's personal experience of learning how to structure formal reasoning using the Coq proof assistant and employ Coq in large-scale research projects. The present manuscript offers a brief and practically-oriented introduction to the basic concepts of mechanized reasoning and interactive theorem proving.

The primary audience of the manuscript are the readers 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 manuscript 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 reader 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.

[PDF | GitHub]

On found typos, errors and logical inconsistencies, please, email me.

Citing PnP

  author        = {Ilya Sergey},
  title         = {{Programs and Proofs: Mechanizing Mathematics with Dependent Types}},
  month         = {August},
  year          = {2014},
  note          = {Lecture notes with exercises},
  doi           = {10.5281/zenodo.4996238}

Supplementary materials

Courses taught via PnP


Last modified: Thu Jun 24 17:41:26 +08 2021