[Club2] Master Thesis defense by Dmitriy Traytel--Tuesday Apr. 3, 11 AM, Turing

[Andrei Popescu]

Dear All,  
Dmitriy will defend his Master Thesis the coming Tuesday.  He will discuss a new approach to foundational (co)datatypes in HOL and its implementation in Isabelle.  
Best regards,   Andrei 
Dmitriy Traytel(joint work with Andrei Popescu and Jasmin Christian Blanchette)Foundational, Compositional (Co)datatypes for Higher-Order Logic--Category Theory Applied to Theorem Proving====================================================Tue. Apr. 3, 11:00, MI 00.09.055 ("Alan Turing")  
Higher-order logic (HOL) forms the basis ofseveral popular interactive theorem provers. These followthe definitional approach, reducing high-level specifications tological primitives. This also applies to the support for datatypedefinitions. However, the internal datatype construction usedin HOL4, HOL Light, and Isabelle/HOL is fundamentallynoncompositional, limiting its efficiency and flexibility, and itdoes not cater for codatatypes. 
We present a fully modular framework for constructing(co)datatypes in HOL, with support for mixed mutual andnested (co)recursion. Mixed (co)recursion enables type defini-tions involving both datatypes and codatatypes, such as thetype of finitely branching trees of possibly infinite depth. Ourframework draws heavily from category theory. The key notionis that of a rich type constructor—a functor satisfying specificproperties preserved by interesting categorical operations. Ourideas are formalized in Isabelle and implemented as a newdefinitional package, answering a long-standing user request.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/club2/attachments/20120329/80fe7370/attachment.html>