Teoria da Computação Discussões e debates sobre pesquisas e publicações Data/Horário: sexta-feira, às 10hLocal: Auditório do MAT/UnB Últimas Palestras 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 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 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 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 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 Apresentações Palestras - Teoria da ComputaçãoHistórico de palestras anteriores Secretaria Fale ConoscoRoteiros e ProcedimentosSolicitaçõesTelefones e e-mail Seminários Álgebra Análise Ensino Geometria Mecânica Sistemas Dinâmicos Teoria da Computação Teoria da Probabilidade Teoria dos Números