home search a-z help
University of Cambridge Logic and Semantics Seminar
25 November 2005: Markus Michelbrink
Computer Laboratory > Research > TSG > Logic and Semantics Seminar > 25 November 2005: Markus Michelbrink

Speaker: Markus Michelbrink, University of Swansea
Title: Container, Interfaces, Games
Time: 25 November 2005, 2.00pm
Venue: William Gates Building, room FW11

Michael Abbott, Thorsten Altenkirch, Connor McBride and Neil Ghani developed the notion of container. A container is basically a family of sets indexed by another set. The name container refers to the way these sets are interpreted, namely as shapes and positions. In this view containers can be seen as polymorphic datatypes in which data may be stored at a certain position.

Peter Hancock and Anton Setzer independently developed the notion of interface to introduce interaction (I/O operations) into dependent type theory and to reason about it. Like containers, interfaces give rise to an endofunctor. Interactive programs are then given by coalgebras for this functor. An interface may be seen as an generalised container. A further generalisation leads to the notion of an (interactive) game.

In my talk I will give an overview over all three notions and their basic properties, show how they are related and what theories are needed to reason about them.