Certifying Termination Proofs - the Evolution of IsaFoR/CeTA 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
Lifting the Nominal Commutative Narrowing 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
