POPL 2021 (series) / CoqPL 2021 (series) / The Seventh International Workshop on Coq for Programming Languages /
Towards a Coq Specification for Generalized Algebraic Datatypes in OCaml
Tue 19 Jan 2021 16:15 - 16:30 at CoqPL - Contributed Talks
Generalized algebraic datatypes have been a part of the OCaml type system, but there has been no formal specification of them. In this talk, we present our ongoing work on mechanizing the metatheory of a core language for modern OCaml and formally proving the soundness of 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.11.
| Abstract (coqpl21-final2.pdf) | 397KiB |
Tue 19 JanDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
Tue 19 Jan
Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
16:00 - 17:30 | |||
16:00 15mTalk | A Limited Case for Reification by Type Inference CoqPL Jason Gross MIT CSAIL Media Attached File Attached | ||
16:15 15mTalk | Towards a Coq Specification for Generalized Algebraic Datatypes in OCaml CoqPL File Attached | ||
16:30 15mTalk | Record Updates in Coq CoqPL Tej Chajed Massachusetts Institute of Technology, USA Media Attached File Attached | ||
16:45 15mBreak | Break CoqPL | ||
17:00 15mTalk | The B+-tree Index as a Verified Software Unit CoqPL Anastasiya Kravchuk-Kirilyuk Harvard University, Andrew W. Appel Princeton, Lennart Beringer Princeton University File Attached | ||
17:15 15mTalk | Automated Synthesis of Verified Firewalls CoqPL Shardul Chiplunkar Massachusetts Institute of Technology, Clément Pit-Claudel Massachusetts Institute of Technology, USA, Adam Chlipala Massachusetts Institute of Technology File Attached | ||