RSS Meetups are monthly gatherings of LASIGE members with research interests mainly in Software Architecture, Verification, Testing, Programming Languages, Type Systems, Logic, Concurrency, and Formal Methods.

Abstract: In this talk I will present Ferrite, a shallow embedding of session types in Rust. In contrast to existing session type libraries and embeddings for mainstream languages, Ferrite not only supports linear session types but also shared session types. Shared session types allow sharing (aliasing) of channels while preserving session fidelity (preservation) using type modalities for acquiring and releasing sessions.
Ferrite adopts a propositions as types approach and encodes typing derivations as Rust functions, with the proof of successful type-checking manifesting as a Rust program.
During the talk, I will present the Ferrite DSL and sketch how it is realized in Rust through a range of advanced type-level features such as lenses and prisms, which allow us to represent linearity (on top of Rust’s affine system) and N-ary labelled choices; and, type-level fixed point combinators, which enable (nested) recursive and shared session types in Rust.

Bio: Bernardo Toninho is an Assistant Professor at Faculdade de Ciências e Tecnologia, Universidade Nova de Lisboa and an integrated member of the PLASTIC research group at NOVA LINCS.
His research focuses on language-based techniques applied to the development of more robust and safer computational systems, with an emphasis on concurrent and distributed systems. More specifically, his work is framed within the realm of advanced type theories (e.g. substructural type theories and dependent type theories) and their application to real-world programming and verification problems.
Bernardo has a PhD in Computer Science by Carnegie Mellon University and Universidade Nova de Lisboa (dual degree) on the logical foundations of session-based concurrent computation, MSc in Computer Science from CMU and FCT-UNL and a BSc in Computer Science from FCT-UNL.