Discussões e debates sobre pesquisas e publicações
Nesta palestra, discutimos os primeiros desenvolvimentos de pares de tuplas funcionais, ou seja, um método de interpretação para reescrita de ordem superior e programação funcional.
Deivid Vale - Radboud University Nijmegen em 24/09/2021
Nesta palestra apresento swaddling, uma técnica de mixed-embedding que nos permite modelar GADTs em OCaml como Inductive Datatypes em Coq.
Pedro da Costa Abreu Purdue University em 15/10/2021
Nesta palestra apresentaremos o módulo do problema da anti-unificação as teorias equacionais vazias, associativas e comutativas. Mostraremos as regras de simplificação de cada um desses casos e as discutiremos por meio de exemplos, apontando os diferentes resultados obtidos para cada teoria equacional. O objetivo é analisar as propriedades de terminação, confluência e correção dos algoritmos anti-unificação.
Gabriela de Souza Ferreira PPGMAT- UnB em 22/10/2021
Esta palestra discute como modificamos o algoritmo seminal de unificação AC de Stickel para evitar a recursão mútua e formalizamos sua terminação e solidez no assistente de prova PVS.
Gabriel Silva PPGINF- UnB em 29/10/2021
