### 12th Wessex Theory Seminar

The twelfth meeting of the Wessex Theory Seminar will take place on Thursday 15 September 2011 at the Queen Mary, University of London.

Venue: Seminar Room BR 4.2 (Computer Science Building, fourth floor, entrance via Bancroft Road).

If you can arrive early, we will be having lunch at Mucci's (inside Campus, opposite Library) from 12 o'clock.

### Abstracts

#### Timothy Griffin: Building Algebraic Structures with Combinators

I'll describe ongoing work with my student Vilius Naudziunas on a domain-specific language for implementing various algebraic structures (semirings, ordered semigroups, etc). Expressions in the language are made up of
constants (representing simple algebras such as min-plus) and combinators that construct new structures from components (such as direct and lexicographic products).

The key feature of the language is that it has been designed so that a fixed class of important properties (such as distributivity, idempotence, commutativity, and so on) are automatically proved or refuted by the type system of the language. This allows a user to specify complex algebraic structures and obtain these proofs (or refutations) automatically. It is hoped that the language and its implementation will facilitate the rapid exploration of the algebraic design space.

We have implemented a prototype using the Coq theorem prover. All of the essential theorem proving — for the "typing rules" — is performed at "language design time." Users writing algebraic expressions at "specification time" do not run Coq directly. Rather, they run code that has been extracted automatically from the (constructive) proofs of our library of Coq theorems.

#### Martin Escardo: A Proof of Omniscience in Agda

The widely quoted Limited Principle of Omniscience (LPO) is not provable in constructive mathematics, and in particular in ML Type Theory (or in Agda, hopefully).

However, if you suitably enlarge the set of natural numbers with a point at infinity, then you get a set that constructively satisfies the principle of omniscience, in all varieties of constructive mathematics.

Here is a proof written in Agda:

http://www.cs.bham.ac.uk/~mhe/papers/omniscient/AnInfiniteOmniscientSet.html

(Given my track record of using Agda in funny ways, I emphasize that this formal proof (1) doesn't disable the termination checker, (2) doesn't use postulates, (3) doesn't rely on translations of classical proofs into intuitionistic proofs, etc. It is in the purest possible fragment of Agda, corresponding to traditional ML Type Theory.)

A proof in human notation is also available in a reference given in the above link. I will present both versions of the proof in the talk, and show that in fact there are plenty of infinite sets that satisfy the principle of omniscience in all varieties of constructive mathematics.

#### Florent Balestieri: Partial Polymorphic Stream Functions

Partial polymorphic stream functions are characterised by their (partial) indexing function which maps elements of the result stream to elements of the input streams. We can define stream functions with mutual recursive equations using primitives 'cons', 'head' and 'tail'. We show that such equations are in fact expressive enough to define all the partial polymorphic stream function.

### Attendance

From Altran Praxis:
Martin Brain

From Bath:
Martin Churchill
Anupam Das
Guy McCusker
John Power
Cai Wingfield
Jim Laird

From Birmingham:
Liang-Ting Chen
Dan Ghica
Martin Escardo
Paul Blain Levy

From Cambridge:
Pierre Clairambault
Tim Griffin
Jonathan Hayman
Ramana Kumar

From Imperial:
Fredrik Dahlqvist

From Nottingham:
Florent Balestieri

From Oxford:
Catrin Campbell-Moore

From QMUL:
Rob Arthan
Paul Curzon
Dino Distefano
Luca Fossati
Peter O'Hearn
Paulo Oliva
Kaustubh Nimkar
Edmund Robinson
Mark Shellhase
Jules Villard
Rasmus L. Petersen
Pasquale Malacaria

From Sussex:
Martin Berger

See all Wessex sites involved and meetings so far.