[Club2] Wed. Oct 27, 14:00: Andrei Popescu

[Alexander Krauss]

Dear all,

In two weeks, Andrei will give a talk on his ideas about improving 
datatypes.

Note: For all those who lost track of all the upcoming talks, I have set 
up a calendar, which (if it turns out to be useful) could become the 
official Club2 calendar:
http://www.google.com/calendar/embed?src=se6ebe3toff4ch5nmunibm5m98%40group.calendar.google.com


A plan for modular (co)datatypes for Isabelle/HOL
======================================================
Wed. Oct 27, 14:00, MI 00.09.055 ("Alan Turing")


Abstract: I propose a revision of the Isabelle datatype package based
on category theory.  The main idea is to store, with each "uniform" type
constructor, further categorical structure(as are, e.g., the "map" and
"set" functions for the "list" type constructor) and a few basic
properties (e.g., that "map" preserves function composition) and then
build the initial algebra (for induction/recursion) and the final
coalgebra (for coinduction/corecursion) purely in terms of this
structure.  This would result in the availability of arbitrarily nested
recursive and corecursive datatypes, where nestedness would be handled
modularly, without having to inline the definitions of the nested
constructors.