[Club2] talk by Dmitriy Traytel--Wed. June 20, 2 PM, Turing

[Andrei Popescu]

Dear All, 
This Wednesday, Dmitriy will have a rehearsal for his LICS talk on HOL (co)datatypes.    
Best regards,    Andrei 
Dmitriy TraytelFoundational, Compositional (Co)datatypes for Higher-Order Logic -- Category Theory Applied to Theorem Proving====================================================Wed. June 20, 14:00, MI 00.09.055 ("Alan Turing")  
Interactive theorem provers based on higher-order logic (HOL) traditionally follow the definitional approach, reducing high-level specifications to logical primitives. This also applies to the support for datatype definitions. However, the internal datatype construction used in HOL4, HOL Light, and Isabelle/HOL is fundamentally noncompositional, limiting its efficiency and flexibility, and it does not cater for codatatypes.
We present a fully modular framework for constructing (co)datatypes in HOL, with support for mixed mutual and nested (co)recursion. Mixed (co)recursion enables type definitions involving both datatypes and codatatypes, such as the type of finitely branching trees of possibly infinite depth. Our framework draws heavily from category theory. The key notion is that of a bounded natural functor - an enriched type constructor satisfying specific properties preserved by interesting categorical operations.
This is joint work with Andrei Popescu and Jasmin Blanchette.  
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/club2/attachments/20120616/a45426a8/attachment.html>