June 28th, at 11:00, Room FC6 146 (S4), Department of Computer Science, FCUP
Please register: https://forms.gle/n4DitMMzcavgw2ZW6
Abstract
In this talk, we are going to show how recent approaches to static analysis based on quantitative typing systems can be extended to programming languages with a global state. More precisely, we are going to present a CBV version of the λ-calculus equipped with operations to deal with a global memory, along with a quantitative model (presented as a tight type system) that captures exact measures of time and space for the evaluation of programs. The validity of the model is ensured by showing that the type system is quantitatively sound and complete with respect to the operational semantics of the language.
Short biography
Miguel Ramos is PhD student at DCC@FCUP and IRIF@UParis, under the supervision of Sandra Alves (DCC@FCUP) and Delia Kesner (IRIF@UParis). His work mainly focuses on using non-idempotent intersection types (quantitative types) to build resource aware semantics (quantitative relational models) for different extensions of the λ-calculus.
About Talks@DCC :
The mission of the Talks@DCC seminars is to bring together researchers and students, to foster discussions and promote scientific awareness and collaboration. Participate: attend and propose your talk.