PLACES 2024 Programme and Proceedings
The PLACES 2024 proceedings are published in volume 401 of EPTCS.
6 April 2024
Parc Alvisse Hotel, Room: Holenfells
| 8:00-9:00 | Arrival and registration | |
| 9:00-9:10 | Opening of PLACES 2024 | |
| 9:10-10:00 | Keynote talk | Peter Müller, ETH Zurich, CH. Verified Secure Routing |
| 10:00-10:30 | Coffee break | |
| 10:30-11:05 | Session: Networking and Semantics Chair: Felix Stutz | Samuel Cavoj, Ivan Nikitin, Colin Perkins and Ornela Dardha. Session types for the transport layer: towards an implementation of TCP |
| 11:05-11:40 | Simon Fowler, Philipp Haller, Roland Kuhn, Sam Lindley, Alceste Scalas and Vasco T. Vasconcelos. Behavioural Types for Heterogeneous Systems (Position Paper) | |
| 11:40-12:15 | Ilaria Castellani and Paola Giannini. Towards a semantic characterisation of global type well-formedness | |
| 12:30-14:00 | Lunch | |
| 14:00-14:50 | Keynote talk | Mariangiola Dezani-Ciancaglini, Università di Torino, IT. Simple MultiParty Sessions |
| 14:50-15:00 | Mini break | |
| 15:00-15:35 | Session: Session subtyping Chair: Alceste Scalas | Thien Udomsrirungruang and Nobuko Yoshida. Three Subtyping Algorithms for Binary Session Types and their Complexity Analyses |
| 15:35-16:00 | Elaine Li, Felix Stutz and Thomas Wies. Multiparty Session Type Projection and Subtyping with Automata | |
| 16:00-16:30 | Coffee break | |
| 16:30-17:05 | Session: Session-typed programming Chair: Raymond Hu | Pedro Ângelo, Atsushi Igarashi and Vasco Vasconcelos Session-typed Metaprogramming |
| 17:05-17:30 | Lasse Nielsen and Nobuko Yoshida. Hapi - Implementing the asynchronous π-calculus with multiparty session types | |
| 17:30-17:55 | Walid Nawfal Sabihi, Martin Vassor and Nobuko Yoshida. Multiparty Session Type Inference for a Rust DSL | |
| 17:55-18:00 | Closing | |
Keynote Talk: Verified Secure Routing
Peter Müller (ETH Zurich, CH)
SCION is a new Internet architecture that addresses many of the security vulnerabilities of today’s Internet. Its clean-slate design provides, among other properties, route control, failure isolation, and multi-path communication. The verifiedSCION project is an effort to formally verify the correctness and security of SCION. It aims to provide strong guarantees for the entire architecture, from the protocol design to its concrete implementation. The project uses stepwise refinement to prove that the protocol withstands increasingly strong attackers. The refinement proofs assume that all network components such as routers satisfy their specifications. This property is then verified separately using deductive program verification in separation logic. This talk will give an overview of the verifiedSCION project and explain, in particular, how we verify code-level properties such as memory safety, I/O behavior, and information flow security.
Keynote Talk: Simple MultiParty Sessions
Mariangiola Dezani-Ciancaglini (Università di Torino, IT)
Simple MultiParty Sessions (SMPS) do not have channels, session initiators and the distinction between compile time and run time syntax. They are based only on participant names and input/output processes. They are equipped with global types without requiring projections and local types. In this presentation we will discuss pros and cons of SMPS. On the good side SMPS allow to easily describe internal delegation, partial typing and session composition. On the bad side SMPS are less espressive than standard MultiParty Sessions. In particular interleaved sessions with crossing delegations cannot be represented.