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 Coq
Palestrante: Pedro da Costa Abreu Purdue University
Data: 15/10/2021