[Club2] Rehearsal talks: Wed., July 9, starting from 11:30, Room: Turing (00.09.38)

[Dmitriy Traytel]

Hi All,

because of a paper deadline on Tuesday, I've changed my mind: I will 
join the marathon as well. Let's say after Peter 14:20-15:10.

But I don't want to force codatatypes on anybody, so everybody (except 
for coauthors) is free to skip my rehearsal.

Dmitriy

Title: Truly Modular (Co)datatypes for Isabelle/HOL
Abstract:
We extended Isabelle/HOL with a pair of definitional commands for
datatypes and codatatypes. They support mutual and nested (co)recursion 
through
well-behaved type constructors, including mixed recursion--corecursion, 
and are
complemented by syntaxes for introducing primitively (co)recursive functions
and by a general proof method for reasoning coinductively. As a case 
study, we
ported Isabelle's Coinductive library to use the new commands, 
eliminating the
need for tedious ad hoc constructions.

On 07.07.2014 01:08, Andrei Popescu wrote:
> After Julian's talk, we have the ITP and Isabelle Workshop rehearsal 
> talks:
>
> Julian: 11 -- 11:30
>
> Lars N: 11:30 -- 11:50
>
> Peter: 13:30 -- 14:20
>
> (remaining free slots: 11:50 -- 12:30 and 14:20 -- 16:00; for extreme 
> cases, also 18 -19)
>
> Andrei
>
>
> On Monday, July 7, 2014 12:59 AM, Andrei Popescu <uuomul at yahoo.com> wrote:
>
>
> Dear All,
>
> On Wednesday we start our marathon with Julian's Master thesis 
> presentation.
>
> Best regards,
> Andrei
>
> Implementation and Verification of Partial Order Reduction for 
> On-The-Fly Model Checking
> Julian Brunner
> ======================================================================
> Wed., July 9, 11:00, Room: Turing (00.09.38)
>
> We present our effort of formally verifying the on-the-fly partial
> order reduction technique described in [Combining Partial Order
> Reductions with On-the-Fly Model-Checking, Doron Peled, Formal Methods
> in System Design, 1996] using the proof assistant Isabelle in
> conjunction with the HOL logic library. First, we briefly introduce
> the idea of partial order reduction. The on-the-fly partial order
> reduction algorithm we want to formalize is built on top of an
> off-line partial order reduction algorithm. Thus, we first present the
> implementation and verification of significant parts of this off-line
> partial order reduction algorithm. Next, we describe the architecture
> of the correctness proof for the on-the-fly partial order reduction
> algorithm. There, we point out a problem with one of the proof steps
> and provide a counterexample showing that the proof of this step is
> not valid. Finally, we give an overview of the formal theories and
> present ideas for further work.
>
>
> On Sunday, July 6, 2014 12:35 PM, Tobias Nipkow <nipkow at in.tum.de> wrote:
>
>
> Andrei,
>
> When you announce Julian's talk on Monday, please do so separately and 
> send a
> copy to Javier who may also want to forward it to his group.
>
> Thanks
> Tobias
>
>
>
>
>
>
> _______________________________________________
> 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/20140707/0481c64d/attachment.html>