Foundations of Programming Meetings

In this talk, I will explore some choices that arise if one wants to design a programming language from scratch, with the intention of supporting software verification.

I will describe Hoare Type Theory (HTT) which integrates a dependently typed higher-order language, with Hoare-like specifications for reasoning about mutable state and pointer aliasing. The lack of this integration in the past has arguably been one of the most significant obstacles in the application of Hoare-style verification methodology, since it prevented effective reasoning about constructs for data abstraction, information hiding, and code reuse.

From the technical standpoint, it is interesting that the design of HTT relates in an essential way some of the most venerable ideas from language theory , which have so far largely existed in isolation, like Dijkstra's predicate transformers, Curry-Howard isomorphism, monads, as well as the more recent idea of Separation Logic.

We have formally proved that HTT is modular, in the sense that the verification of individual program components suffices to establish the correctness of the whole program. HTT is also (almost) conservative over the programming practice in modern functional languages; if the verification features are not used, HTT very much looks like core Haskell.

I will talk about a way to give a useful denotational semantics to type and effect systems. I will show how to extend Plotkin and Power's interpretation of effectful programs as elements of a free universal algebra to incorporate type information that restricts the effects that are allowed at any point in the program.

The idea that bound variables and free (global) variables should be represented by distinct syntactic classes of names goes back at least to Gentzen and Prawitz. In the early 1990's, McKinna and Pollack formalized a large amount of the metatheory of Pure Type Systems with a representation using two classes of names. This work developed a style for formalizing reasoning about binding which was heavy, but worked reliably. However, the use of names for bound variables is not a perfect fit to the intuitive notion of binding, so I suggested (1994) that the McKinna--Pollack approach to reasoning with two species of variables also works well with a representation that uses names for global variables, and de Bruijn indices for bound variables. This \emph{locally nameless} representation, in which alpha equivalence classes have exactly one element, had previously been used in Huet's Constructive Engine and by Andy Gordon. The locally nameless representation with McKinna--Pollack style reasoning has recently been used by several researchers (with several proof tools) for solutions to the POPLmark Challenge.

This talk will give an overview of the technique for extracting computational content from proofs emphasising the gab between the pure method that works in principle and refined techniques that can be applied to nontrivial examples with practically useful results. We will focus on programs from classical proofs involving choice principles and further show how program extraction can be successfully applied to algorithm verification.