Functional Tuple Pairs and Applications to Higher-Order Complexity Theory 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
Traduzindo Generalized Algebraic Datatypes (GADTs) de OCaml para Coq 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
Anti-unification modulo syntactic, associative and commutative equational theories 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
A Certified Sound Algorithm for AC-unification 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
