Yuting Wang
where else to find them
no profile links on file
what they talk about
where they keep going back
- POPL3 editions2022–2025
on a stage with
all 9 in the filters
who talks about the same things
- Ling Zhang4 talks
- Jérémie Koenig4 talks
- Zhong Shao19 talks
- Youngju Song6 talks
- Adam Chlipala23 talks
- Yizhou Zhang13 talks
| title | conference | date |
|---|---|---|
| CompCertOC: Verified Compositional Compilation of Multi-threaded Programs with Shared(…) | PLDI 2025 | 2025-06-16 |
Claim: a verified compiler that compositionally preserves semantics for cooperative multi-threaded C programs that share stack data. Key techniques are… | ||
| Unifying compositional verification and certified compilation with a three-dimensional(…) | POPL 2025 | 2025-01-19 |
A concrete claim: a three-dimensional algebra of refinement composes module interfaces, abstraction levels, and state views so compiler correctness, linking… | ||
| Fully Composable and Adequate Verified Compilation with Direct Refinements betwe... | POPL 2024 | 2024-01-14 |
Claims a Kripke Memory Relation (called NGP) that is transitive and absorbs per-pass rely/guarantee conditions so a single direct refinement relates Clight… | ||
| Verified Compilation of C Programs with a Nominal Memory Model | POPL 2022 | 2022-01-16 |
The paper claims a drop-in generalization of CompCert’s block memory model into a nominal memory model that uses atoms/supports to rename and separate blocks… | ||
| CompCertELF: Verified Separate Compilation of C Programs into ELF Object Files | OOPSLA 2020 | 2020-11-15 |
CompCertELF is a Coq-verified C-to-ELF toolchain that adds a verified assembler and supports verified separate compilation by proving commutativity between… | ||
| nothing matches | ||