[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]
Call for Participation - Iris Workshop 2019 Aarhus University - October 28-29, 2019 Dear All, On October 28-29, we are hosting the Iris Workshop 2019 at the Department of Computer Science, Aarhus University. It is a specialist workshop focusing on Iris-related research, but we welcome participation by anyone who is interested. Find more information about the workshop here: https://iris-project.org/workshop-2019/ and find out more about Iris here: https://iris-project.org Participation in the workshop is free, but you need to register your participation at https://events.au.dk/iris2019 (deadline: October 11). All participants are welcome to stay 1-3 days longer for more informal discussions and interaction. PRELIMINARY PROGRAM: October 28 09:00 - 10:00: Invited talk: Ralf Jung: Logical Atomicity in Iris: The Good, the Bad, and the Ugly 10:00 - 10:30: Coffee break 10:30 - 11:00: Amin Timany: Aneris: A Logic for Node-Local, Modular Reasoning of Distributed Systems 11:00 - 11:30: Jesper Bengtson: Actris: Session-Type Based Reasoning in Separation Logic 11:30 - 12:00: Rodolphe Lepigre: TBA 12:00 - 13:30: Lunch 13:30 - 14:30: Invited Talk: François Pottier: Playing spy games in Iris 14:30 - 15:00: Léo Stefanesco: TBA 15:00 - 15:30: Coffee and cake 15:30 - 16:00: Philippa Gardner: Compositional Reasoning for the Termination of Fine-grained Concurrent Programs 16:00 - 17:00: Invited Talk: Gregory Malecha: TBA 18:30 - 21:30: Conference dinner at No. 16 (https://no16.nu/) October 29 09:00 - 10:00: Invited talk: Dan Frumin: Compositional Non-Interference for Fine-Grained Concurrent Programs 10:00 - 10:30: Coffee break 10:30 - 11:00: Glen Mével: Iris for Multicore OCaml 11:00 - 11:30: Armaël Guéneau: Formal verification of an incremental cycle detection algorithm 11:30 - 12:00: Andrew Appel: Recent developments in the Verified Software Toolchain 12:00 - 13:30: Lunch 13:30 - 14:30: Invited Talk: Bart Jacobs: Specifying I/O using Abstract Nested Hoare Triples 14:30 - 15:00: Aïna Linn Georges: Implementing a Capability Machine model into Iris 15:00 - 15:30: Coffee and cake 15:30 - 16:00: Paolo Giarrusso: Step-Indexed Logical Relations for (guarded) Dependent Object Types 16:00 - 16:30: Hai Dang: RustBelt Relaxed Best wishes, Robbert Krebbers and Lars Birkedal -- Lars Birkedal Villum Investigator Professor, Head of Logic and Semantics Group Dept. of Computer Science Aarhus University Aabogade 34 8200 Aarhus N Denmark birke...@cs.au.dk<mailto:birke...@cs.au.dk> www.cs.au.dk/~birke