Por João Barbosa
No dia 28 de abril, às 16h00, no anfiteatro FC6 0.29, João Barbosa dará uma palestra intitulada "Tipos Regulares e as suas Propriedades".
Título
Tipos Regulares e as suas Propriedades
Resumo
Tipos regulares são tipos que podem ser descritos por uma gramática de termos regular. Estes correspondem a conjuntos recursivos de termos ground que têm interseção, comparação e teste de vazio decidíveis. Foram extensivamente usados como tipos para programação em lógica, porque são facilmente implementados com programas lógicos. Adicionalmente, estão relacionados com tipos de dados algébricos, que são extensivamente usados em programação funcional. Várias operações e propriedades de tipos regulares foram formalizadas e usadas em inferência de tipos, com sucesso limitado. Vamos também estender esta definição adicionando variáveis e descobrindo onde nos leva esta extensão em termos de expressividade e decidibilidade de operações.
Bio
João Barbosa tem um doutoramento em Ciência de Computadores pela Faculdade de Ciências da Universidade do Porto e é Professor na mesma instituição. Começou a sua investigação a tentar descrever uma disciplina de tipos para programação em lógica, que é tipicamente não-tipada. A sua tese de mestrado baseou-se no conceito de tipos regulares e um subconjunto destes, chamados tipos fechados. No seu doutoramento, descreveu uma semântica de três valores para programação em lógica, um sistema de tipos e um algoritmo de inferência de tipos que inferem tipos (regulares) fechados. Também descreveu uma semântica operacional tipada para programação em lógica, baseada na mesma lógica de três valores, e descreveu como pode ser extendida da semântica operacional tradicional para programação em lógica (resolução SLD) e usada para detetar erros de tipos em programas e em queries.
Recentemente descreveu um algoritmo de unificação tipado e implementou um interpretador Prolog que usa a semântica operacional tipada que desenvolveu durante o doutoramento e o algoritmo de unificação tipado. A implementação é em Maude, um framework de lógica de reescrita. Também está atualmente a usar autómatos de árvore para obter mais algoritmos para tipos regulares, ao relacionar ambos. Esta relação vai ser formalizada usando um assistente de prova, Lean.