[ 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
[email protected]<mailto:[email protected]>
www.cs.au.dk/~birke