A TRANSLATION OF OCAML GADTS INTO COQ ...
Purdue University Graduate School, 2024
Hochschulschrift
Zugriff:
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. When that language is sufficiently similar to that of the proof assistant, one solution is to use a shallow embedding to directly encode source programs as programs in the proof assistant. One challenge with this approach is ensuring that any semantic gaps between the two languages are accounted for. In this thesis, we present 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. We formalize this with GADTml, a minimal calculus that captures GADTs in OCaml, and gCIC, an impredicative variant of the Calculus of Inductive Constructions. Furthermore, we present the ...
Titel: |
A TRANSLATION OF OCAML GADTS INTO COQ ...
|
---|---|
Autor/in / Beteiligte Person: | Junior, Pedro da Costa Abreu |
Link: | |
Veröffentlichung: | Purdue University Graduate School, 2024 |
Medientyp: | Hochschulschrift |
DOI: | 10.25394/pgs.25665378 |
Schlagwort: |
|
Sonstiges: |
|