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