XVIII Seminário Informal (, mas Formal) do GTC-UnB

The XVIII Informal (, but Formal!) Seminar of the GTC-UnB will be integrated to the Summer Workshop in Mathematics - UnB, organized by the Department of Mathematics at University of Brasília. It will be an online event occurring in the period 09-11, February, 2021.

Past editions can be found here.

Time: 14:30- 15:30 ( UTC-3)

Categorical Models of Explicit Substitutions -

Valeria de Paiva (Topos Institute and DI-Puc-Rio)

Abstract: In this talk, we explore recent approaches to quantitative typing systems for programming languages with pattern matching features. Quantitative (non-idempotent intersection) types have been used to characterise solvability for a pair pattern calculus, in which a qualitative characterisation of head-normalisation was given by means of typability.

We show that one can go further and provide upper-bounds/exact measures for head-normalisation, by means of two resource- aware quantitative type systems (system U and system E), which take advantage of specific technical tools. While system U provides upper bounds for the length of head-normalisation sequences and the size of normal forms, system E goes even further and produces exact measures for each of them, as well as discriminating between the different kind of reduction steps performed.

The general program, including plenary talks and poster sessions, can be found in https://www.mat.unb.br/verao2021/programa_en.html

Talks