Joomy Korkut
where else to find them
bluesky:joomy.bsky.social
what they talk about
where they keep going back
no series more than once — all 4 in the filters
on a stage with
- Andrew W. Appelonce
- Kathrin Starkonce
- Matthew Z. Weaveronce
who talks about the same things
nobody close enough yet
| title | conference | date |
|---|---|---|
| Crane Lowers Rocq Safely into C++ | RocqPL 2026 | 2026-01-17 |
Crane extracts Rocq into idiomatic, readable C++ that maps Rocq inductive types and monadic effects to either stdlib or Bloomberg core types, generates… | ||
| A Rose Tree is Blooming (Proof Pearl) | CPP 2026 | 2026-01-12 |
Compares two implementations of rose-tree unfolding in the Rocq prover: an inductive version requiring a well‑founded relation and accessibility proofs, and a… | ||
| A Verified Foreign Function Interface Between Coq and C | POPL 2025 | 2025-01-19 |
VeriFFI provides a verified foreign-function interface that translates Coq dependent types and Coq functional models into VST specs so C functions, once proved… | ||
| Lightning talk: Commanding Emacs from Coq | Scheme 2019 | 2019-08-18 |
Defines a monadic eDSL in Coq that models atomic editor actions (get-char, remove-char, insert-char) and builds an Emacs Lisp interpreter that talks to Coq… | ||
| nothing matches | ||