**10th Wessex Theory Seminar**

The tenth meeting of the Wessex Theory Seminar took place on Thursday, 7. April 2011 in Swansea.

Lectures were given in Robert Recorde Room (Far-205), Faraday Building (= big blue building to the right on the campus), at Swansea University.

There was a light buffet lunch available from 12:30 onwards for people arriving for the seminar.

**Preliminary Programme**

##### 12:30 Lunch

##### 13:30 Martin Escardo: The ubiquitous selection monad.

##### 14:20 Paulo Oliva: The dialectica interpretation of classical logic, arithmetic and analysis

##### 15:00 Break

##### 15:30 Martin Brain: An Algebra of Search Spaces

##### 16:10 Ondrej Rypacek: Higher Dimensional Type Theory

##### 16:40 Peter Mosses: PLanCompS - Programming Language Components and Specifications

##### 17:00 Closing

**Abstracts**

#### Martin Escardo: The ubiquitous selection monad.

This is part of a fruitful ongoing research programme, jointly developed with

Paulo Oliva, which is characterized by the slogan "selection functions everywhere".

I'll present the theory of selection functions, and discuss its role in

game theory, proof theory, topology, higher-type computation, among others.

Selection functions form a strong monad, which can be defined in any

cartesian closed category, and has a morphism into the continuation

monad. In certain categories of domains or spaces, the strength can be

infinitely iterated. This infinite strength is an amazingly versatile

functional that (i) optimally plays sequential games, (ii) realizes

the Double Negation Shift used to realize the classical axiom of

countable choice, and (iii) implements a computational version of the

Tychonoff Theorem from topology. The infinite strength turns out to be

built-in in the functional language Haskell, called sequence, and can

be used to write unexpected programs that compute with infinite

objects, sometimes surprisingly fast. The selection monad also gives

rise to a new translation of classical logic into intuitionistic

logic, which we refer to as the Peirce translation, as monad algebras

are objects that satisfy Peirce's Law.

#### Paulo Oliva: The dialectica interpretation of classical logic, arithmetic and analysis

In this survey talk I will show, through simple examples, how Gödel's dialectica

interpretation allows for the extraction of programs from classical proofs. We will

start with simple theorems from classical predicate logic, and then move into

more complex theorems involving induction and countable choice. The novel

aspect of the talk will centre around the use of the product of selections 1,2 to

obtain direct and readable programs.

1 Martín Escardó and Paulo Oliva, Selection functions, bar recursion and backward induction.

Mathematical Structures in Computer Science, 20(2):127-168, 2010

2 Martín Escardó and Paulo Oliva, Sequential games and optimal strategies.

Proceedings of the Royal Society A, 2010

#### Martin Brain: An Algebra of Search Spaces

This talk presents an overview of an ongoing program of

research aiming to produce a representation-independent formalism for

reasoning about search problems and the algorithms used to solve them.

Unlike previous approaches, the focus of this work is on formalising the

notion of search space rather than just the parts of the space explored

by given algorithms. Algebraic structures, I-Spaces, are used to

represent search spaces so that the results are syntax and language

independent. The basic definition of I-Spaces, a model of computation

and an algebraic semantics for CSPs are given as an illustration of this

approach.

#### Ondrej Rypacek: Higher Dimensional Type Theory

I will present an ongoing work, joint with Thorsten Altenkirch, on

foundations of Martin-Löf Type Theory which is addressing the question

whether equality of types can be isomorphism or a related notion. Such

a "Higher Dimensional Type Theory" would make it easy to reason about

mathematical concepts up to isomorphism.

A paradigmatic example is that of a vector space which can be

equivalently represented by any of its bases. While it is convenient

to work with any particular base, it is equivalently important that

the choice is irrelevant in the sense that all choices give rise to

the same structure. Currently, this is not possible in Intensional

Type Theory as different bases give rise to coercible but not

extensionally equal vector spaces. In computer science, one routinely

needs to model programming structures which are extensional, however

some concrete syntax is required for definition of programs over the

structures. In greater generality, the problem is the definition of

elimination constants which are irrelevant of the choice made in the

representation.

This work is inspired by a proposal by Vladimir Voevodsky on univalent

models of type theory which is also related to recent results by

Garner & van den Berg and Lumsdaine on the weak omega groupoid model

of Type Theory. Our goal is to develop a syntactic theory, which is

computationally well behaved, which supports higher dimensional

Identity Types (i.e. uniqueness of identity proofs doesn't hold) and

which supports extensional reasoning about functions. The upshot of

such a theory would be to seamlessly integrate axiomatic definitions

of mathematical structures in terms of variables, operations and

equations on the one hand and their model theoretic presentations

which work with a chosen representation in a given semantic domain, on

the other hand. An example is Type Theory itself; a faithful model of

which is still an open and bothering problem.

#### Peter Mosses: PLanCompS - Programming Language

Components and Specifications

PLanCompS is a 4-year EPSRC-funded joint research project between

Swansea, Royal Holloway and City, with Microsoft Research Cambridge

as a project partner, starting mid-2011. It is to establish and test the

practicality of a component-based framework for the design, specification

and implementation of programming languages. The main novelty will be

the creation of a substantial collection of highly reusable, validated language

components called fundamental constructs (funcons). Crucially, the

semantic specification of each funcon will be independent, not needing any

reformulation when funcons are combined or new funcons added to the

collection; specifying a translation of a language to funcons will define both

the static and dynamic semantics of the language. All specifications will be

provided online in an open access repository, with browsing and searching

supported by a digital library interface.

This talk gives a brief presentation of the project, which is about to

recruit three (preferably postdoc) research assistants and two PhD students.

**Attendance**

From Bath:

Martin Brain

Martin Churchill

Pierre Clairambault

Guy McCusker

John Power

Cai Wingfield

From Birmingham:

Liang-Ting Chen

Martin Escardo

Olaf Klinke

From Imperial:

Fredrik Dahlqvist

Bjoern Lellmann

From Queen Mary:

Paulo Oliva

From Swansea:

Arnold Beckmann

Ulrich Berger

Roger Hindley

Tie Hou

Andrew Lawrence

Peter Mosses

Monika Seisenberger

John Tucker

From King's:

Ondrej Rypacek

See all Wessex sites involved and meetings so far.