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 Abstract Assistentes de prova baseados em tipos dependentes (e.g. Coq e Lean) são ferramentas poderosas para se construir softwares corretos. No entanto, para se verificar programas escritos em uma linguagem diferente, é necessário construir uma representação deste programa no assistente de prova.Quando a linguagem original do programa é similar o suficiente com a linguagem do assistente de prova, podemos utilizar uma técnica conhecida como shallow embedding para representar estes programas de forma direta na linguagem do assistente de prova. Um dos problemas desta abordagem é que qualquer diferença entre a semântica destas linguagens precisa ser levado em conta.Nesta palestra apresento swaddling, uma técnica de mixed-embedding que nos permite modelar GADTs em OCaml como Inductive Datatypes em Coq. Esta técnica nos permite traduzir a riqueza de informação embutido na tipagem de GADTs sem perder a expressividade de pattern matching com impossible branches e sem recorrer ao uso de axiomas adicionais. Nós integramos esta técnica em coq-of-ocaml, uma ferramenta utilizada para traduzir automaticamente programas de OCaml para Coq. E demonstramos a utilidade de nossa abordagem utilizando esta implementação para traduzir para Coq uma porção da base de códigos da cryptomoeda Tezos. Local e Data Tema: Traduzindo Generalized Algebraic Datatypes (GADTs) de OCaml para CoqPalestrante: Pedro da Costa Abreu Purdue UniversityData: 15/10/2021 Secretaria Fale ConoscoRoteiros e ProcedimentosSolicitaçõesTelefones e e-mail Seminários Álgebra Análise Geometria Mecânica Sistemas Dinâmicos Teoria da Computação Teoria da Probabilidade Teoria dos Números