Invited Talk: Resource-Aware Session Types
This talk presents recent work on extending session types to describe and enforce resource constraints.
First, I briefly review the use of session types for prescribing bidirectional communication protocols for message-passing processes. Then, I show how session types can be combined with the potential method of amortized analysis to account for the (sequential) work performed by a process. Next, I discuss temporal session types, which uniformly express properties such as the message rate of a stream or the latency of a pipeline and can be used to reason about parallel complexity. Finally, I discuss the application of these resource-aware session types in Nomos, a programming language for digital contracts.
I am a Tenure-Track Assistant Professor at Carnegie Mellon’s Computer Science Department, and a member of the Principles of Programming (PoP) group.
My research areas are programming languages and formal methods. I am specifically interested in quantitative verification, type systems, static resource analysis of programs, proof assistants, and system verification.
Before joining Carnegie Mellon, I was an Associate Research Scientist in the Department of Computer Science at Yale. Before that, I was a PhD student at LMU Munich.
Sun 13 Jan
|13:30 - 14:20|
Jan HoffmannCarnegie Mellon University
|14:20 - 15:10|
Invited Talk: A Session Type Provider: Compile-time Generation of Session Types with Interaction Refinements
Rumyana NeykovaBrunel University LondonFile Attached
|15:10 - 15:30|
Hans HüttelDepartment of Computer Science, Aalborg University, Antonio RavaraDepartment of Informatics, Faculty of Sciences and Technology, NOVA University of Lisbon and NOVA LINCS, Adrian FrancalanzaUniversity of Malta, Mario BravettiUniversità di BolognaFile Attached