Nosso objetivo nesta palestra é estender um dos resultados mais importantes do estreitamento – o Teorema do Elevação – para o arcabouço nominal considerando o caso comutativo. Em particular, discutiremos as dificuldades para obter provas de exatidão e completude neste cenário de comutatividade módulo estreitamento nominal.
Daniella Santaguida - UnB em 25/03/2022

Esta palestra cobrirá uma visão geral do certificador CeTA, cuja solidez foi comprovada em Isabelle/HOL. Começaremos com a fase inicial em que o CeTA foi usado exclusivamente para verificar as provas de terminação dos sistemas de reescrita de termos e, em seguida, continuaremos com os desenvolvimentos recentes que desencadearam o desenvolvimento de um solucionador SMT totalmente verificado para aritmética linear inteira.
René Thiemann - Computational Logic Group University of Innsbruck em 05/11/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

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

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