Foundations of Programming Meetings
School of Computer Science and ITUniversity of Nottingham
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).
Matthieu Sozeau,
University of Paris XI
Jeremy Gibbons,
Oxford University
James Brotherston,
Imprial College, London
Eugenia Cheng,
University of Sheffield
Further Information
Meetings are normally held on Fridays at 2 p.m. in room C1 in
the School of Computer Science on the Jubilee Campus.
On-line directions to the Jubilee Campus are available, and our address is as
follows:
School of Computer Science and IT
University of Nottingham
Jubilee Campus, Wollaton Road
Nottingham NG8 1BB
United Kingdom