Logics of higher order than programming verified in Coq

Documents and media

Download support

pdf (2.51 MB)

Abstract

This lecture completes the previous one by ending the presentation of general methods for proving programs with one based on higher-order logics (those where we can also quantify on predicates) and on the lambda-calculus already presented in detail in the 2009-2010 lecture. First, we show why higher-order logic is more expressive than first-order logic. For example, to prove a property by recurrence, in predicate calculus we need a recurrence axiom scheme that generates a particular axiom for each predicate to be studied, and therefore an infinite number of axioms; in higher order, a single standard axiom suffices, since we can universally quantify the working predicate. Other advantages will become apparent as the lecture continues. One disadvantage, of course, is the greater complexity of the logic and of some of the algorithms used to process it.

First, we'll briefly describe M. Gordon's HOL, J. Harrison's HOL-Light, N. Shankar, S. Owre and J. Rushby's PVS, and L. Paulson's Isabelle, the latter being a meta-logic system in which several logics can be defined. These systems have led to very important proofs in practice: the integer and floating-point arithmetic correction proof of Intel's Pentium by J. Harrison after the famous Pentium Pro division bug that cost Intel $470 million in 1994; the seL4 operating system micronucleus correction proof performed by G. Klein et. al. at NICTA Sydney using Isabelle (cf. D. Bolignano's seminar on March 11, 2015 for another operating system proof).

We then present in more detail the Coq system, developed in France and the recipient of major recent awards. Coq is based on the CoC construction calculus by G. Huet and T. Coquand (1984) and its inductive CiC version developed by C. Paulin, who will speak in a seminar following this lecture. Coq differs from classical systems in that it completely integrates computation and proof in a very rich formalism, incorporating and considerably developing ideas and theorems by de Bruijn (Automath, 1967), Girard (SystemF, 1972), etc.

Gallina, Coq's programming language is a higher-order typed language, i.e., its types can themselves be functions. Typing is decidable, and the type system guarantees that all computations of well-typed terms end in unique normal forms. Classical programming is facilitated by the inductive layer, which enables powerful recursive definitions with guaranteed termination. Thanks to the implementation of the fundamental Curry-Howard correspondence between computation and proof, there is no longer any real difference between computation and proof. For example, the type of a program is its specification, while the type of a proof is the theorem it proves, in exactly the same way. What's more, proofs are standard calculus functions, just like functions on classic data types. Finally, once a program has been developed and proven in Coq, we can automatically extract directly executable object code written in Caml, which is correct by construction and normally efficient. All this gives Coq a considerable richness for specifying, programming, proving and exporting, four activities that become completely integrated.

The lecture will conclude with the presentation of two major Coq successes: firstly, the CompCert certified compiler by X. Leroy's CompCert-certified compiler, the only C compiler to have passed the random testing filter presented in the lecture on March 4; and secondly, the completely formal proof of major mathematical theorems by G. Gonthier et al.