The Foundations of Programming group holds regular research meetings. The meetings last around an hour, and are intended to be a friendly forum for discussion and exchange of ideas. Most meetings take the form of a talk by a group member or an invited speaker, but we also have various kinds of discussion sessions. The meetings are open to everyone, not just members of the group. Please contact Neil Ghani if you are interested in visiting the group and giving a talk.
Details of previous years meetings are also available: 1995; 1996; 1997; 1998; 1999; 2000; 2001; 2002. 2003. 2004. 2005. 2006. 2007.
Details of recent and upcoming meetings are given below.
A universe is a type of types, and somehow the primordial form of type-dependency. There's quite a variety of them, from Jan Smith's "microscopic" Boolean universe, the bog standard ones, Peter Morris's universes for generic programming, Erik Palmgren's universes of higher-order operators, and Anton Setzer's Mahlo universe. I'll take you on a tour of some of these, and point out some of their salient features. My idea is that rolling your own universes will become as mundane as rolling your own datatypes. I'll try my best to be intelligible to folk not greatly up on type theory. (No promises.)
There exist different methods for developing certified programs in the Coq environment. The standard one is to use Coq's language as a simply typed, purely functional language and prove properties about the programs in the usual way. Another, lesser known approach, is to use the complete Coq language to specify and implement programs, making invariants, pre- and post-conditions appear in the types of terms. This method is generally overlooked because it is difficult to cope with in practice as algorithms and proofs become entangled using dependent types. The Program system tries to solve this problem by reconciling the two approaches. It consists of a language (Russell) which permits writing purely algorithmical code with rich specifications, a sound translation from Russell terms to Coq terms which generates proof obligations and a mechanism for handling these. I will present these three components and show how we can extend the system to handle real examples (live).
The judgements in this system express (guaranteed) termination of the program from a given point and under a given precondition, which is expressed using separation logic. The proof rules of our system are then of two types: logical rules that operate on preconditions; and symbolic execution rules that capture the effect of executing program commands.
A proof in our system, however, is not the usual finite tree of judgements, but rather a cyclic proof: a regular infinite tree, represented as a cyclic graph, that satisfies a global soundness condition. Essentially, this soundness condition stipulates that some inductive predicate is unfolded infinitely often along every infinite path, thus allowing us to discard all potentially infinite program computations by an infinite descent argument. Moreover, the use of this soundness condition enables us to avoid the usual explicit use of ranking functions for termination.
Our proof system is supported by appropriate soundness and completeness theorems, and by examples in which non-trivially terminating programs have been proven terminating for the first time under our approach.
This is joint work with Richard Bornat (Middlesex) and Cristiano Calcagno (Imperial).
School of Computer Science and IT
University of Nottingham
Jubilee Campus, Wollaton Road
Nottingham NG8 1BB
United Kingdom