Colloquium of Logic  RSS

Planned

14/11/2024, 17:00 — 18:00 Europe/Lisbon — Room P3.10, Mathematics Building Instituto Superior Técnicohttps://tecnico.ulisboa.pt
, Departamento de Ciência de Computadores, Faculdade de Ciências

Quantitative Weak Linearisation

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.

Email announcements subscription

This seminar series has an active subscriber list. It is used by the seminar organizer to publicize events. To request or cancel membership add your name and email below. Depending on your address being on the list or not you will be able to unsubscribe or subscribe.

Data submission

Logo SPL