Author: Thorsten Altenkirch
Title: Codata
Abstract: 
We discuss the rule of codata, i.e. coinductively defined
datatypes, in Type Theory. Our basic idea is the symmetry
between a producer contract for data which allows us to program
with and reason about data and a consumer contract which allows
us to deal with codata. Our analysis also reopens the question
of extensionality.