Son Ho
where else to find them
what they talk about
where they keep going back
- ICFP2 editions2022–2023
on a stage with
who talks about the same things
nobody close enough yet
| title | conference | date |
|---|---|---|
| Incremental Proof Development in Dafny with Module-Based Induction | Dafny 2024 | 2024-01-14 |
Claim: encoding Coq-style induction principles as module-based induction in Dafny makes iterative proofs stable and debuggable. Implementation: a list… | ||
| Modularity, Code Specialization, and Zero-Cost Abstractions for Program Verifica... | ICFP 2023 | 2023-09-04 |
Implements a userland F metaprogram that performs whole-call-graph code specialization for Low and compiles to readable C, producing an extra compiler stage… | ||
| Aeneas: Rust Verification by Functional Translation | ICFP 2022 | 2022-09-11 |
Aeneas translates a large, safe subset of Rust (no interior mutability or unsafe) into a pure lambda calculus so proofs avoid memory/address reasoning… | ||
| nothing matches | ||