School of Computer Science
University of Nottingham
Thursday, 27 May 2010, 14:00
Cybernetica Bldg (Akadeemia tee 21), room B101
Code from the talk [agda (embedded in html)]
Abstract: Both inductive definitions and coinductive definitions play an important role in functional programming and constructive reasoning. Examples include inductive datatypes like lists, inductive relations like provability, coinductive datatypes like streams and coinductively defined relations like bisimilarity. However, frequently we encounter datatypes and relations where we want to use both induction and coinduction. We will discuss a number of example using the dependently typed language Agda as a vehicle. Agda supports mixed inductive and coinductive definitions but there are also some unresolved issues with our approach. In particular, it is not yet clear how to support deeper nesting of mixed definitions.
(Based on joint work with Nils Anders Danielsson.)