No próximo dia 12 de maio de 2021 pelas 13h30, Sandra Alves, docente no DCC-FCUP irá dar uma palestra intitulada "A quantitative understanding of pattern matching".
A palestra é organizada pelo DCC-FCUP e pelo grupo de investigação CRACS-INESC TEC e é aberta a todos os interessados.
A sessão será de forma remota, a participação é gratuita. O link da sessão será partilhado a pedido.
Short Bio
Sandra Alves long term focus of research in the study and development of models and tools for analysis and verification of computational systems using type-theory, rewriting and fundamental calculi, with a particular interest in models that implicitly or explicitly deal with resources. having completed her PhD 2007. Her PhD thesis, completed in 2007, dealt with type-systems for linear languages, for which she received a Distinction for Young Researchers from Calouste Gulbenkian Foundation. She has published several papers in major international conferences and in major international journals. Sandra Alves has maintained activities at editorial boards of journals (MSCS and FLAP), steering committees (RTA, Linearity, LSFA, FSCD) an executive board (IFCoLog), organisation of events (DiL’12, Linearity’12, Logic Colloquium’13, Linearity’14, FSCD’16, LSFA’17, DCM’18, WiL’20, WiL’21) and programme committees (Linearity’09, Linearity’12, CiE’14, Linearity’14, LSFA’14, PPDP’16, LSFA’17, LSFA’18, LSFA’19, TyDE’19, IWC’19, WiL’19, CSL’20, LSFA’20, FSCD’20, FOSSACS’21, LSFA’21, IWC’21, MFPS’21).
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 takes 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 kinds of reduction steps performed.