Xuanrui Qi
where else to find them
what they talk about
where they keep going back
no series more than once — all 3 in the filters
on a stage with
who talks about the same things
nobody close enough yet
| title | conference | date |
|---|---|---|
| Formalizing OCaml GADT typing in Coq | ML 2021 | 2021-08-26 |
Mechanization of OCaml GADT typing in Coq formalizes ambivalent-type principality and proves subject reduction for a graph-based encoding; implementation… | ||
| Towards a Coq Specification for Generalized Algebraic Datatypes in OCaml | CoqPL 2021 | 2021-01-19 |
Formalizes OCaml GADT behavior by building a Coq mechanization of a core ML with structural polymorphism, recursive types and type-level equality; finds a… | ||
| Towards a Coq Specification for Generalized Algebraic Datatypes in OCaml | POPL 2021 | 2021-01-17 |
A Coq mechanization of OCaml-style GADTs targets a core language with structural polymorphism, recursive types and type-level equality witnesses (OCaml 4.11)… | ||
| nothing matches | ||