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

[Alexander Krauss]

Silke talked me into giving away our usual room this week. Therefore, 
the talk will be in MI 01.11.018 ("Konrad Zuse").


Alexander Krauss wrote:
> 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.
>