Palestra [07/10]: Mario Florido (UPorto)

[Daniel Ventura]

O Grupo de Estruturas Formais, Fundamentos e Aplicações (EFFA/UFG), em associação ao Grupo de Teoria da Computação (GTC/UnB), convida-os à participação do seminário remoto dos grupos de pesquisa em temas relacionados aos Fundamentos em Computação e Matemática Aplicada à Computação.

Título: Substructural Type Systems and Intersection Types

Palestrante: Mario Florido (Universidade do Porto)

Resumo: Types are now widely used as specifications for correctness properties of programs. However the standard type systems in use are usually not powerful enough to specify properties which limit the ordering and the number of uses of computational resources. Substructural type systems give us this extra power of controlling the number and order of uses of computational resources.

Intersection types originate in the works of Barendregt, Coppo and Dezani and give us a characterization of the strongly normalizable terms, in the sense that a term is typed in an intersection type system  if and only if it is strongly normalizable. These systems type more terms than the Curry type system and the Damas-Milner type system.

In this talk we will address the following problem: to which extent can we approximate a typed term in the intersection type system by terms typable in a simpler type system, such as the Curry Type System or a substructural type system? 

We will present a notion of term expansion, which generalises expansion as used before to linearize the strongly normalizable terms. Under this notion we will show that one can define terms with less sharing, but with the same computational properties of terms typable in an intersection type system. We will then show that expansion relates terms typed by an intersection type with terms typed in the Curry Type System and several substructural type systems, tuning the degree of sharing by choosing different algebraic properties of the intersection operator.

Data: 08 de outubro de 2021 (sexta-feira)

Horário: 10:00 (UTC-3)

Link: https://us02web.zoom.us/j/89412679078?pwd=ZjV6b3BvaGYwNFVLWXJaTWd6TjVWZz09

Meeting ID: 894 1267 9078
Passcode: 310030