ProgLog Meetings in 2009

Past meetings of 2009.

Date Speaker Title Extra
Nov 18 Miroslav Dobsicek Quantum computing, and the reversal between computer science and natural science.
Nov 11 Ross Paterson [EDIT room] Applicative functors from left Kan extensions abstract
Jun 10 Stevan Andjelkovic, Linus Ek, Ola Holmström Implementing self-balancing binary search trees in Agda
May 27 Thierry Vilmart Probability Logic
Mar 18 Pierre Clairambault A game-theoretic framework for dependent types abstract
Mar 11 Miguel Pagano A modular type-checking algorithm for Type Theory abstract
Feb 25 Conor McBride Slicing it: indexed containers? in Haskell? abstract
Feb 20 Bas Spitters A computer-verified implementation of Riemann integration - an introduction to computer mathematics abstract
Feb 19 Peter Aczel Identity Types and Type Setups abstract
Feb 5 Peter Dybjer On the thesis by Johan Granström: "Reference and Computation in Intuitionistic Type Theory"


Abstracts of talks in 2009


Formalising the Odd-Even merge-sort algorithm

Date: Dec 2
Speaker: Ana Bove
Abstract:
The odd-even merge-sort algorithm was developed by K.E. Batcher in 1968. It is based on a merge algorithm that merges two sorted sequences to a completely sorted sequence. This is a general recursive algorithm where the number of comparisons is in O(n.(log n)^2). In contrast to usual merge-sort algorithm, the odd-even merge-sort algorithm is not data-dependent, i.e. the same comparisons are performed regardless of the actual data in each position of the sequences. Proofs of correctness of this algorithm usually make use of the 0-1 principle and reason about the number of 0's in the sequences. In this talk I will present and explain the algorithm, how we can informally convince ourselves of its correctness and how to implement and prove this algorithm correct in type theory.


[EDIT room] Applicative functors from left Kan extensions

Date: Nov 11
Speaker: Ross Paterson
Abstract:
Applicative functors define an interface that is more general, and correspondingly weaker, than that of monads. First used in parser libraries, they are now seeing a wide range of applications. Left Kan extensions, familiar to functional programmers as a kind of existential type, are a source of a range of applicative functors that are not also monads. There is also a generalized form involving arrows, which appears in the permutation parsers of Baars, Loh and Swierstra.


A game-theoretic framework for dependent types

Date: Mar 18
Speaker: Pierre Clairambault
Abstract:
We present a construction of a category Dep of dependent games and valid total strategies. We turn then to an analysis of dependency through a class of monotonic relations, representing external dependency. With these, we enrich the category Dep with the fibred structure of a Category with Families. We show that our category with families supports intensional identity types, which makes it a sound model of intensional type theory.


A modular type-checking algorithm for Type Theory

Date: Mar 11
Speaker: Miguel Pagano
Abstract:
In the talk I will present a joint work (abstract follows) with Andreas Abel and Thierry. At the end I will show the modularity of the technique considering a type corresponding to the free abelian monoid on the singleton set.

Abstract: We define a logical framework with singleton types and one universe of small types. We give the semantics using a PER model; it is used for constructing a normalisation by evaluation algorithm. We prove completeness and soundness of the algorithm; and get as a corollary the injectivity of type constructors. Then we give the definition of a correct and complete type-checking algorithm for terms in normal form. We extend the results to proof-irrelevant propositions.


Slicing it: indexed containers? in Haskell?

Date: Feb 25
Speaker: Conor McBride (Strathclyde University)
Abstract:
In this talk I shall attempt to explain the idea of "indexed containers" - a key foundational component of dependent data structures. Improbably, I shall seek to do this by developing the basic equipment for constructing and using them in a dialect - fictitious, but plausible enough to be executable already - of the dependently typed functional programming language, Haskell.

A container F : Set -> Set gives sets F X which behave like collections of elements drawn from X. We expect containers to be functorial, i.e. to support

map_F : all S, T. (S -> T) -> F S -> F T

and, moreover, to have least (greatest) fixpoints corresponding to (co-)inductively defined sets, equipped with (un-)fold operators and so on. Recursively defined containers may then be studied (in the style of Bird, de Moor et al.) by taking fixpoints of two-parameter containers with bifunctorial structure, and so on.

In the dependently typed setting, we can generalize to the notion of indexed container (Altenkirch, Ghani, Hancock, McBride, and Morris) G : (I -> Set) -> (O -> Set), for sets I of "input" kinds of element and O of "output" kinds of collection, with at least the functorial behaviour suggested by seeing each (X -> Set) as a slice category

map_G : all X, Y. (all i. X i -> Y i) -> (all o. G X o -> G Y o)

E.g., vectors are indexed containers in (1 -> Set) -> (Nat -> Set), with one kind of element, and collections distinguished by length; map for vectors transforms elements, preserving length. Conveniently, indexed containers are closed under fixpoints. Correspondingly, their "algebra of programming" is arguably rather more straightforward in principle than for the standard "set, functor, bifunctor, .." presentation.


A computer-verified implementation of Riemann integration - an introduction to computer mathematics

Date: Feb 20
Speaker: Bas Spitters
Abstract:
The use of floating point real numbers is fast, but may cause incorrect answers due to overflows. These error can be avoided by hand. Better, exact real arithmetic allows one to move this bookkeeping process entirely to the computer allowing one to focus on the algorithms instead. For maximal certainty, one uses a computer to check the proof of correctness of the implementation of this algorithm. We illustrate this process by implementing the Riemann integral in constructive mathematics based on type theory. The implementation and its correctness proof were driven by an algebraic/categorical treatment of the Riemann integral which is of independent interest.
This work builds on O'Connor's implementation of exact real arithmetic. A demo session will be included. (Joint work with Russell O'Connor)


Identity Types and Type Setups

Date: Feb 19
Speaker: Peter Aczel
Abstract:
In the first part of my talk I will review some of the rules for identity types that have been considered and discuss how they are related to each other when Pi and Sigma types are not available in the type theory.

In the second part of the talk I will introduce the notion of a type setup. This is an abstraction from the notion of a (dependent) type theory in which types and terms are abstract while contexts are kept as sequences of variable declarations. The notion is closely related to Peter Dybjer's notion of a category with families. But while that notion treats contexts as abstract objects of a category and is intended as giving a notion of possible mathematical semantics for type theories, the notion of a type setup is intended to capture an abstract syntactic notion of type theory at a more concrete level of abstraction. I believe that the notion of a type setup can be used to conveniently express some results of Richard Garner concerning identity contexts.