No próximo dia 12 de Dezembro, pelas 14h30 na sala FC6 146 do DCC FCUP, Sandra Alves irá dar uma palestra intitulada "Quantitative Weak Linearisation".
A palestra é organizada pelo DCC-FCUP.
Short Bio
Sandra Alves's research has been 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. 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 is associated editor of the CUP Journal on Mathematical Structures in Computer Science, an executive officer of ACM SIGLOG and IFCoLog, and is a member of the IFIP working group on rewriting. She has served in the steering of committees of several conferences and workshops (TLCA, FSCP, TYPES, Linearity, LSFA, WiL) and has a strong involvement in the research community, having participated in the organisation and served in the program committee of dozens of events.
Title
Quantitative Weak Linearisation
Abstract
Weak linearisation was defined years ago through a static characterisation of the intuitive notion of virtual redex, based on (legal) paths computed from the (syntactical) term tree. Weak-linear terms impose a linearity condition only on functions that are applied (consumed by reduction) and functions that are not applied (therefore persist in the term along any reduction) can be non-linear. This class of terms was shown to be strongly normalising with deciding typability in polynomial time. We revisit this notion through non-idempotent intersection types (also called quantitative types). By using an effective characterisation of minimal typings, based on the notion of tightness, we are able to distinguish between “consumed” and “persistent” term constructors, which allows us to define an expansion relation, between general lambda-terms and weak-linear lambda-terms, whilst preserving normal forms by reduction.