Wednesday, 3/6/09, C60, 1400 - 1500
Andy Gill, (University of Kansas)
Typedirected Observational Sharing
Haskell is a great language for writing and supporting embedded Domain Specific Languages (DSLs). Some form of observable sharing is often a critical capability for allowing so-called deep DSLs to be compiled and processed. In this talk, I describe and explore uses of an IO function for reification which allows direct observation of sharing.
Friday, 1/5/09, C60
Christian Wüthrich, (University of Nottingham)
Some questions in computational number theory
I indent to give an introductory overview on some questions in computational number theory, focusing on the resolution of Diophantine equations. These are polynomial equations with integer coefficients, like y^2 = x^3 +2x^2-3x. We are interested in deciding if there is an integer solution, or a rational solution, and if so how many are there, ... In end, I would like to illustrate some of the results with the computer algebra software 'sage'
Friday, 17/4/09, C60
Ondrej Rypacek, (University of Nottingham)
Distributive Laws for Programming Structures
Distributive laws in Category Theory have originally been defined for a pair of monads as a means of combination of algebraic structures. In the Category Theory of Computer Science different variants of the original notion have been defined and formally studied. In programming, distributive laws are rules governing when data and/or program structures can be transformed from one form into another; surprisingly many programming techniques exploit such rules. However, despite their ubiquitousness, as yet a useful general theory of distributive laws doesn't exist. Such a theory would make it possible to identify and exploit the commonalities of the specific examples.
In the talk, formal 2-categorical foundations of a general theory of distributive laws will be presented. In particular, the notion of a morphism of a functor with additional structure will be formalised, and a general notion of a distributive law of functors with additional structure will be defined. Its basic properties will be studied in order to support the claim that this is the right and formally sound approach. The presentation will concentrate on examples and the simple geometric nature of the 2-categorical notions.
Friday, 27/3/09, C60
Alexander Kurz, (University of Leicester)
An Introduction to Coalgebraic Logic
Coalgebras are dual to algebras and provide a general account
of processes and dynamic systems, giving rise to the research programme
of Universal Coalgebra, initiated by Rutten. In this talk we will see
how to treat logics for coalgebras in such a framework. The aim is to
have, at the same time, an abstract approach working uniformly for all
types of coalgebras and to deal with concrete logics (described by
particular syntax) and their properties. The main idea is the following:
Coalgebras are given wrt to a `type functor' T, an abstract logic for
coalgebras of type T is given by a functor L dual to T, a concrete logic
is given by a syntactic presentation of L. Hennessy-Milner logic would
be a typical example of a logic arising in this way.
Friday, 27/2/09, C60
Peter Hancock, (University of Nottingham)
Eating: beyond streams
`Eating' is about writing programs that implement functions on final
coalgebras, typically stream types. The crucial thing is to do it in
a composable way, as with Unix-style piping.
I'll quickly canter through stream eating, pointing out the use of
nested fixedpoints, and of universal properties to define things.
The main content of the talk is about
eating `infinite' objects that inhabit the final coalgebras of
container functors. For a long time I was stuck on how to do this in
a composable way; a few days ago I cracked it, and would like to show
you. You can regard it as a study in dependently typed programming,
in which quite a few interesting things emerge.
Friday, 20/2/09, C60
Thomas Anberree, (University of Nottingham in Ningbo)
Non-deterministic programs for real numbers.
Semantical proof of universality.
We consider a functional language with a type for the real
numbers and a non-deterministic operator. A real number is
outputted as a sequence of finer and finer rational intervals
[p,q]. Because the test r>0 is not decidable, a redundant test
Rtest:Real->Bool is used, which detects which of r>0 and r<1
hold. If both may be detected to hold, either True or False is
We present a possible semantics based on powerdomains (roughly:
a program is denoted by a set representing its possible
results). Despite lacking the adequacy property one usually
expects, the semantics is good enough to prove that computable
functions R-->R are definable in the language.
Friday, 6/2/09, C60
Peter Jonsson, (Luleå University of Technology)
Positive Supercompilation for a Higher Order Call-By-Value Language
Clear and concise programs written in functional programming languages
often suffer from poor performance compared to their counterparts
written in imperative languages such as Fortran or C.
Supercompilation is a program transformation that can mitigate many of
these problems by removing intermediate structures and perforing
Previous deforestation and supercompilation algorithms may introduce
accidental termination when applied to call-by-value programs. This
hides looping bugs from the programmer, and changes the behavior of
a program depending on whether it is optimized or not. We present a
supercompilation algorithm for a higher-order call-by-value language
and report on our current work of implementing it in the Timber compiler.
We also prove that the algorithm both terminates and preserves
termination properties of the input program. This algorithm utilizes
strictness information for deciding whether to substitute or not and
compares favorably with previous call-by-name transformations.
Friday, 30/1/09, C60
Richard Garner, (University of Cambridge)
Two-dimensional models of type theory
It is well-known that there is a correspondence between locally cartesian closed categories and extensional dependent type theories (at least modulo issues concerning substitution). The question of how to extend this correspondence to deal with intensional dependent type theories is still open. Whilst there are notions of categorical model for intensional type theory, these do not do much more than to recast the syntax in a categorical language; in particular, they do not give a suitable analogue of the one-dimensional characterisation of dependent sum and product as left and right adjoint to substitution.
In this talk, we take a step along the road towards such a notion of model. We define a class of "two-dimensional" intensional type theories, and show that they correspond to a certain kind of 2-categorical model in which dependent sum and product may be characterised by (bicategorical) left and right adjoints to substitution.
Friday, 16/1/09, C60
Johan Jeuring, (University of Utrecht)
Generic programming with fixed points for mutually recursive datatypes
Many datatype-generic functions need access to the recursive positions in the
structure of the datatype, and therefore adopt a fixed point view on datatypes.
Examples include variants of fold that traverse the data following the
recursive structure, or the zipper data structure that enables navigation along
the recursive positions. However, Hindley-Milner-inspired type systems with
algebraic datatypes make it difficult to express fixed points for anything but
regular datatypes. Many real-life examples such as abstract syntax trees are
in fact systems of mutually recursive datatypes and therefore excluded. Using
Haskell's GADTs and type families, we describe a technique that allows a
fixed-point view for systems of mutually recursive datatypes. We demonstrate
that our approach is widely applicable by giving several examples of generic
functions for this view, most prominently the Zipper.
Friday, 21/11/08, C60, 1400 - 1500 (changed time!)
Ralf Hinze (University of Oxford)
Scans and Convolutions
A Calculational Proof of Moessner's Theorem
In this talk, I introduce two co-recursion schemes for
stream-generating functions, scans and convolutions, and discuss their
properties. As an application of the framework, a calculational proof
of Paasche's generalisation of Moessner's intriguing theorem is
Friday, 14/11/08, C60
Conor McBride (University of Strathclyde)
Ornamental Algebras, Algebraic Ornaments
The best-kept secrets in dependently typed programming
are that "lists are natural numbers with labelled successors"
and "vectors are lists indexed by their length". I mean that
we tend to keep these facts secret from the computer, if not
from each other, and then we complain about how much work it
is to relate these structures. In this talk, I'll show how to
let the computers in on these secrets by giving a coding
scheme which can express how to construct one datatype by
ornamenting another. Remarkably, if we express the first
secret as an ornament, the machine can compute the ornament
for the second secret. The "reuse problem" has just become
the "reuse opportunity".
Friday, 17/10/08, C60
Nicola Gambino (University of Leicester)
The identity type weak factorisation system
Martin-Löf type theory is generally studied in mathematical
logic as a foundation for constructive mathematics and in theoretical
computer science as a dependently-typed programming language. The
seminar will take a different point of view: we investigate what may
be referred to as the homotopy theory of Martin-Löf type theory. I
will show how the syntax of Martin-Löf type theory gives rise to a
category that admits a non-trivial weak factorisation system. I will
then relate this weak factorisation system the natural Quillen model
structure on the category of groupoids. No prior knowledge of homotopy
theory will be required. This is joint work with Richard Garner.
S. Awodey and M. A. Warren, Homotopy-theoretic models of identity
types. ArXiv:0709.0248. To appear in Mathematical Proceedings of the
Cambridge Philosophical Society.
N. Gambino and R. Garner, The identity type weak factorisation system.
ArXiv:0803.4349. To appear in Theoretical Computer Science.
Friday, 10/10/08, C60
John Power (University of Bath)
Structural Operational Semantics for Computational Effects
(joint with Gordon Plotkin)
In seeking a unified study of computational effects, a fundamental task is to give a unified structural operational semantics, together with an adequate denotational semantics for it, in such a way that, for the leading examples of computational effects, the general definitions are consistent with the usual operational semantics for the relevant effects. One can readily produce a unified operational semantics that works fine for examples that include various forms of nondeterminism and probabilistic nondeterminism. But that simple semantics fails to yield a sensible result in the vitally important case of state or variants of state. The problem is that one must take serious account of coalgebraic structure. I shall not formally enunciate a general operational semantics and adequacy theorem in this talk, but I shall explain the category theory that supports such a semantics and theorem.
I shall investigate, describe, and characterise a kind of tensor of amodel and a comodel of a countable Lawvere theory, calculating it in leading examples, primarily involving state. Ultimately, this research supports a distinction between what one might call coalgebraic effects, such as state, and algebraic effects, such as nondeterminism.
Friday, 12/9/08, C1
Sam Staton (University of Cambridge)
Towards general structural operational semantics, through categorical logic.
One can start with known set-theoretic results for simple process languages, such as congruence of bisimulation. By considering these standard results in more elaborate settings, such as presheaf categories, we achieve results that are relevant for more elaborate languages.
The talk will be partly based on my paper at LICS this year
(The talk will be accessible to a general theoretical computer science audience.)