Joshua M. Cohen
where else to find them
no profile links on file
what they talk about
where they keep going back
no series more than once — all 2 in the filters
on a stage with
who talks about the same things
nobody close enough yet
| title | conference | date |
|---|---|---|
| Implementing OCaml APIs in Coq | CoqPL 2025 | 2025-01-25 |
Extraction is modified to map Coq encodings of OCaml effects to real OCaml exceptions and refs so extracted code matches existing APIs while remaining… | ||
| A Formalization of Core Why3 in Coq | POPL 2024 | 2024-01-14 |
Formalization of Why3's core logic as a machine-checked denotational semantics in Coq maps Why3 types to Coq sets, builds explicit encodings for recursive… | ||
| nothing matches | ||