Séminaire des équipes de recherche
Units in the OCaml typechecker
- Date : 21/02/2017
- Place : 2 rue Simone Iff (ou: 41 rue du Charolais) - Salle Lions 1, bâtiment C - 15h45
- Guest(s) : Jacques Garrigue (Nagoya University)
14h30 : "Verification of OCaml typing proofs"
Pierrick Couderc (OCamlPro & ENSTA ParisTech)
During type inference, the OCaml compiler builds a type-annotated abstract syntax tree that can be seen as a typing proof. Ideally, a program checking the correctness of those typing proofs should implement the OCaml type discipline, and proving the soundness of this program should establish the soundness of the OCaml type system.
In this talk, I will describe my ongoing work in checking OCaml type-annotated ASTs, and formalizing in Coq the type soundness of a subset of OCaml.
15h45 : "Units in the OCaml type checker "
Jacques Garrigue (Nagoya University)
We introduce an extension of the OCaml typechecker which allows to express units of measurement. It allows to verify the coherence of units in computations, with applications to scientific or financial algorithms. We reuse Kennedy's algorithm for unification of units, but go back to linear algebra to handle type inclusion and equality.
The interaction of this extension with the core algorithm being very small, we also discuss how this could be implemented as a plug-in in the typechecker.
This is joint work with Dara Ly.