A Translation of OCaml GADTs into Coq

Pedro Abreu


Date: Wed, October 02, 2024
Time: 12:00
Room: Turing


Proof assistants based on dependent types are powerful tools for building certified software. In order to verify programs written in a different language, however, a representation of those programs in the proof assistant is required. One challenge with this approach is ensuring that any semantic gaps between the two languages are accounted for.

This work introduces GSet, a mixed embedding that bridges the gap between OCaml GADTs and inductive datatypes in Coq. This embedding retains the rich typing information of GADTs while also allowing pattern matching with impossible branches to be translated without additional axioms. For this, we develop two minimal calculus that captures the essence of our translation algorithm: GADTml and gCIC, and we prove its soundness. We have integrated this technique into coq-of-ocaml, a tool for automatically translating OCaml programs into Coq. Finally, we demonstrate the feasibility of our approach by using our enhanced version of coq-of-ocaml, to translate a portion of the Tezos code base into Coq.

About the speaker

Pedro Abreu (https://pedroabreu0.github.io/) holds a Bachelor’s degree in Computer Science from the University of Brasília. He earned a Master’s degree from Purdue University (Indiana, USA) and is the host of the Type Theory Forall Podcast (https://www.typetheoryforall.com/). He has also completed various internships and consulting work in the areas of testing and formal verification of programs, including at the Federal Court of Accounts (TCU - Brasília), SiFive (San Mateo, Silicon Valley), Galois (Portland, Oregon), Nomadic Labs (Paris), Pruvendo, and others.

Previous: Jasper Denkers |
Next: Peter Mosses |