Thursday, 26 April 2007, 14:00
Cybernetica Bldg (Akadeemia tee 21), room B101
Slides from the talk [pdf]
Abstract: Inductive datatypes like lists or trees can be understood as initial algebras and dually coinductive datatypes like streams correspond to terminal coalgebras. We (Michael Abbott, Neil Ghani, & myself) have introduced the theory of containers to construct such datatypes and also to be able to reason about them generically. In my talk I am going to review the theory of containers and then discuss the question how to extend it to inductive families (like the typed lambda terms). This is ongoing work with Neil Ghani, Peter Hancock, Peter Morris and Conor McBride sometimes summarily referred to as Midlands Containers Ltd.