Logical Foundations Notes


Building reliable software is hard. The developing of large-scale systems are prone to bugs and insecurities. Computer scientists have responded these challenges for improving reliability, using mathematical techniques for specifying and reasoning about properties of software and tools for helping validating these properties. The Software Foundations series is focused on this last set of tools.

This course is based around Coq, which enables a variety of works:

  • As a platform for modeling programming languages.

  • As an environment for developing formally certified software and hardware.

  • As a realistic environment for functional programming with dependent types.

  • As a proof assistant for higher-order logic.

The most basic programming style is to keep the computations pure as much as possible, avoiding side effects such as changes of local states; this makes the programs easier to understand and reason about.

Coq is a proof assistant yet a functional programming language. These two sides of Coq are the reflection of the underlying machinery, that is, proofs are programs.


Chapter 1 Functional Programming in Coq
Chapter 2 Proof by Induction
Chapter 3 Working with Structured Data
Chapter 4 Polymorphism and Higher-Order Functions
Chapter 5 More Basic Tactics
Chapter 6 Logic in Coq
Chapter 7 Inductively Defined Propositions
Chapter 8 Total and Partial Maps
Chapter 9 The Curry–Howard Correspondence