[Club2] Reminder: Dmitriy Traytel's talk today, 11 AM, Turing

[Andrei Popescu]

Regards,    Andrei 

--- On Thu, 3/29/12, Andrei Popescu <uuomul at yahoo.com> wrote:

From: Andrei Popescu <uuomul at yahoo.com>
Subject: Master Thesis defense by Dmitriy Traytel--Tuesday Apr. 3, 11 AM, Turing
To: club2 at mailbroy.informatik.tu-muenchen.de
Date: Thursday, March 29, 2012, 12:22 PM

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/20120403/97a31e6d/attachment.html>