Validating OCaml soundness by translation into Coq
Proving the correctness of a type checker for a full-fledged programming language is a difficult task. As an alternative approach, we consider translating the result of type checking to Coq. The expressiveness of Gallina’s type system allows a type preserving translation, and its strong soundness properties ensures the safety of typed terms. We developed a new backend for a subset of OCaml that generates a Coq version, such that one can verify that the result of their evaluation is the intended one. We plan to extend it to cover a large part of the language.
Tue 10 MayDisplayed time zone: Osaka, Sapporo, Tokyo change
14:00 - 17:00
|Constraint-based Relational and Temporal Verification|
Hiroshi Unno University of Tsukuba; RIKEN AIP
|Validating OCaml soundness by translation into Coq|
Jacques Garrigue Nagoya University