[Club2] Reminder: Nonprimitive Corecursion in Isabelle/HOL @ Thu Jul 16, 2015 14:00 - 15:00 (Club2)

[Dmitriy Traytel]

On 01.07.2015 12:07, julianbrunner at gmail.com wrote:
>
> Event Invitation
>
> Title:
>
> 	
>
> Nonprimitive Corecursion in Isabelle/HOL
>
> Location:
>
> 	
>
> MI 00.09.038 (Turing)
>
> When:
>
> 	
>
> Thu 16 Jul 2015 14:00 – 15:00
>
> 	
> 	
>
> Organizer:
>
> 	
>
> 	Club2 <se6ebe3toff4ch5nmunibm5m98 at group.calendar.google.com>
>
> Description:
>
> 	
>
> Speaker: Aymeric Bouzy Abstract: Codatatypes can be used to model 
> possibly infinite data. They have been introduced in Isabelle/HOL in 
> 2013. Since 2014, there has been a “primcorec” command as well, for 
> defining primitively corecursive functions. We implement a 
> foundational framework for corecursion support, "corec", that offers a 
> lot more syntactic flexibility. In particular, it allows corecursion 
> under "friendly" operations. The command "corec" results in much 
> shorter, more natural definitions: for example, the part of Traytel’s 
> "Coinductive_Languages" entry in the Archive of Formal Proofs that 
> defines regular operations can be shrunk to 12% of its size, without 
> the need to introduce intermediate constants, and without writing a 
> single proof line. View your event at 
> https://www.google.com/calendar/event?action=VIEW&eid=aDM5bjRzczY1MGt1cGptZWY2cThybHRkcWsgY2x1YjJAbWFpbGJyb3kuaW5mb3JtYXRpay50dS1tdWVuY2hlbi5kZQ&tok=NTIjc2U2ZWJlM3RvZmY0Y2g1bm11bmlibTVtOThAZ3JvdXAuY2FsZW5kYXIuZ29vZ2xlLmNvbTA3Zjk4MzVhODcwMThlYTg5M2JmZmExNWQxYjNkMDhjOTIxNTJiNzM&ctz=Europe/Berlin&hl=en.
>
> Comment:
>
> 	
>
> Attendees:
>
> 	
> 	
>
> 	club2 at mailbroy.informatik.tu-muenchen.de 
> <club2 at mailbroy.informatik.tu-muenchen.de>
>
> 	Aymeric Bouzy <aymeric.bouzy at gmail.com>
>
>
>
> _______________________________________________
> Club2 mailing list
> List page: https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/club2
> Webpage with calendar: http://www21.in.tum.de/club2

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/club2/attachments/20150716/73d08e86/attachment.html>