Seminars (2008/2009)
Wednesday, 3/6/09, C60, 1400  1500
Andy Gill, (University of Kansas) Typedirected Observational Sharing Abstract 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 socalled 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 Abstract 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^23x. 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' slides
Friday, 17/4/09, C60 Ondrej Rypacek, (University of Nottingham) Distributive Laws for Programming Structures Abstract 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 2categorical 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 2categorical notions. slides
Friday, 27/3/09, C60 Alexander Kurz, (University of Leicester) An Introduction to Coalgebraic Logic Abstract 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. HennessyMilner 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 Abstract `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 Unixstyle 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. slides
Friday, 20/2/09, C60 Thomas Anberree, (University of Nottingham in Ningbo) Nondeterministic programs for real numbers. Semantical proof of universality. Abstract We consider a functional language with a type for the real numbers and a nondeterministic 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 returned, nondeterministically. 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. slides
Friday, 6/2/09, C60 Peter Jonsson, (Luleå University of Technology) Positive Supercompilation for a Higher Order CallByValue Language Abstract 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 program specialization.
Previous deforestation and supercompilation algorithms may introduce accidental termination when applied to callbyvalue 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 higherorder callbyvalue 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 callbyname transformations. POPL paper
Friday, 30/1/09, C60 Richard Garner, (University of Cambridge) Twodimensional models of type theory Abstract It is wellknown 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 onedimensional 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 "twodimensional" intensional type theories, and show that they correspond to a certain kind of 2categorical model in which dependent sum and product may be characterised by (bicategorical) left and right adjoints to substitution. preprint
Friday, 16/1/09, C60 Johan Jeuring, (University of Utrecht) Generic programming with fixed points for mutually recursive datatypes Abstract Many datatypegeneric 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, HindleyMilnerinspired type systems with algebraic datatypes make it difficult to express fixed points for anything but regular datatypes. Many reallife 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 fixedpoint 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. slides
Friday, 21/11/08, C60, 1400  1500 (changed time!) Ralf Hinze (University of Oxford) Scans and Convolutions A Calculational Proof of Moessner's Theorem Abstract In this talk, I introduce two corecursion schemes for streamgenerating 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 presented. slides
Friday, 14/11/08, C60 Conor McBride (University of Strathclyde) Ornamental Algebras, Algebraic Ornaments Abstract The bestkept 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". Agda code
Friday, 17/10/08, C60 Nicola Gambino (University of Leicester) The identity type weak factorisation system Abstract MartinLöf type theory is generally studied in mathematical logic as a foundation for constructive mathematics and in theoretical computer science as a dependentlytyped programming language. The seminar will take a different point of view: we investigate what may be referred to as the homotopy theory of MartinLöf type theory. I will show how the syntax of MartinLöf type theory gives rise to a category that admits a nontrivial 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. References S. Awodey and M. A. Warren, Homotopytheoretic 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. slides
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. Abstract
One can start with known settheoretic 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 http://www.cl.cam.ac.uk/~ss368/lics08.pdf
(The talk will be accessible to a general theoretical computer science audience.) Slides
