Yong Kiam Tan
where else to find them
no profile links on file
what they talk about
where they keep going back
- CPP3 editions2020–2026
all 4 in the filters
on a stage with
all 12 in the filters
who talks about the same things
- Johannes Åman Pohjola2 talks
- Magnus O. Myreen8 talks
- Oskar Abrahamsson2 talks
- Thomas Sewell2 talks
- Scott Owens2 talks
- Jan Hoffmann9 talks
| title | conference | date |
|---|---|---|
| Verified VCG and Verified Compiler for Dafny | CPP 2026 | 2026-01-12 |
Builds a functional big‑step semantics for an imperative subset of Dafny and proves a verified VCG and verified compiler that translate Dafny (mutual… | ||
| From CakeML to Proof Checking, and Back Again | ML 2025 | 2025-11-24 |
CakeML now comprises about 750,000 lines of code (over a million including auxiliaries) and delivers a formally verified compiler from a high‑level ML-like… | ||
| Cakes That Bake Cakes: Dynamic Computation in CakeML | PLDI 2023 | 2023-06-17 |
Extends the verified CakeML compiler with an Eval primitive that compiles and executes new CakeML code at runtime, letting original and dynamic code share… | ||
| A First Complete Algorithm for Real Quantifier Elimination in Isabelle/HOL | CPP 2023 | 2023-01-16 |
Formal verification of a first complete multivariate QE in Isabelle/HOL that hybridizes Ben-Or‑Kozen‑Reif and Tarski: it reduces quantifier elimination to sign… | ||
| Do You Have Space for Dessert? A Verified Space Cost Semantics for CakeML Programs | OOPSLA 2020 | 2020-11-15 |
Presents a concrete, verified space-cost semantics for CakeML by formalizing a dataLang cost semantics that measures heap and stack with a size_of function… | ||
| The Poincare-Bendixson Theorem in Isabelle/HOL | CPP 2020 | 2020-01-20 |
Formalizes the planar Poincare–Bendixson claim in Isabelle/HOL, building on the existing Jordan curve theorem and ODE/real-analysis libraries. Key result is a… | ||
| nothing matches | ||