Logical Foundations Notes

Preface

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.

Notes

Chapter I   Functional Programming in Coq
Chapter II  Proof by Induction
Chapter III Working with Structured Data
Chapter IV  Polymorphism and Higher-Order Functions
Chapter V   More Basic Tactics
Chapter VI  Logic in Coq
Chapter VII Inductively Defined Propositions