# Foundations of Programming Meetings

School of Computer Science and IT
University 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.

## Speakers 2008

Friday the 1st of February, 2pm, C1
Peter Hancock, University of Nottingham
A rough guide to some universes.
Friday the 15th of February, 2pm, C1
Matthieu Sozeau, University of Paris XI
PROGRAM-ing in Coq
Friday the 22nd of February, 2pm, C1
Jeremy Gibbons, Oxford University
Unfolding Abstract Datatypes
Friday the 7th of March, 2pm, C1
James Brotherston, Imperial College, London
Cyclic Proofs of Program Termination in Separation Logic
Friday the 25th of April, 3:30pm, C1
Eugenia Cheng, University of Sheffield
Terminal Coalgebras

## Abstracts 2008

Friday the 1st of February, 2pm, C1
Peter Hancock, University of Nottingham
A rough guide to some universes.

Friday the 15th of February, 2pm, C1
Matthieu Sozeau, University of Paris XI
PROGRAM-ing in Coq.

Friday the 22nd of February, 2pm, C1
Jeremy Gibbons, Oxford University
Unfolding Abstract Datatypes. One of the most fundamental tools in the programmer's toolbox is the abstract datatype. However, abstract datatypes are not widely used in functional programming, perhaps because they are not subject to familiar proof methods such as equational reasoning and induction - in essence, because they are a form of codata rather than a form of data. We show that proof methods for corecursive programs are the appropriate techniques to use. In particular, building on established work on final coalgebra semantics for object-oriented programs, we show that the reasoning principles of unfold operators are perfectly suited for the task. We illustrate with a solution to a recent problem in the literature.

Friday the 7th of March, 2pm, C1
James Brotherston, Imprial College, London
Cyclic Proofs of Program Termination in Separation Logic. We propose a novel approach to proving the termination of heap-manipulating programs, which combines separation logic with *cyclic proof* within a Hoare-style proof system.

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.

Friday the 25th of April, 3.30pm, C1
Eugenia Cheng, University of Sheffield
Terminal coalgebras (Joint work with Tom Leinster.) Coalgebras for endofunctors may seem rather lacking in structure at first sight - unlike coalgebras for comonads, they satisfy no axioms. However, terminal coalgebras for endofunctors turn out to be rather interesting. A lemma of Lambek tells us that these are fixed points for the endofunctor in question, and a theorem of Adamek gives us an explicit construction, provided we have enough limits and colimits in our ambient category. One consequence is that we have a way of constructing infinite versions of algebraic structures that are usually constructed by induction and thus can usually only be finite. Examples include infinite words, infinite trees and strict $\omega$-categories. In this talk we will present the basic theory and examples, and also give a new example: an $\omega$-dimensional version of Trimble's weak $n$-categories. This talk will not assume knowledge of category theory beyond categories and functors, although familiarity with limits in categories will help.

## 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