ICFP 2021
Sun 22 - Sat 28 August 2021
Thu 26 Aug 2021 20:00 - 20:30 at ML - Compiler & Language Correctness Chair(s): Robert Atkey

The principality of OCaml’s GADT type inference relies on the concept of ambivalence, which allows to reject programs whose typing is ambiguous. Yet, ambivalence itself requires to use a graph view of types, making inductive reasoning more difficult. In this talk, we present our ongoing work on mechanizing the metatheory of a core language for modern OCaml and formally proving soundness and principality for this core language. Our core language supports structural polymorphism, recursive types, and type-level equality witnesses, which are the defining features of OCaml type inference as of version 4.12. We have now proved subject reduction for a meaningful subset of the reduction rules.

Slides (gadt-coq-show.pdf)222KiB

Thu 26 Aug

Displayed time zone: Seoul change

20:00 - 21:30
Compiler & Language CorrectnessML at ML
Chair(s): Robert Atkey University of Strathclyde
Formalizing OCaml GADT typing in Coq
Jacques Garrigue Nagoya University, Xuanrui Qi Nagoya University
Pre-print File Attached
Demo Paper : Coqlex, an approach to generate verified lexers
Wendlasida Ouedraogo Siemens Mobility & Inria Saclay, Danko Ilik Siemens Mobility, Lutz Strassburger Inria Saclay & LIX, Ecole Polytechnique
Media Attached File Attached
Code Extraction from Coq to ML-like languages
Danil Annenkov Concordium Blockchain Research Center, Aarhus University, Mikkel Milo Concordium Blockchain Research Center, Aarhus University, Bas Spitters Aarhus University
Link to publication File Attached