Magnus O. Myreen
where else to find them
no profile links on file
what they talk about
where they keep going back
- PLDI Workshop Honoring Andreas Podelski2 editions2023–2024
all 6 in the filters
on a stage with
all 17 in the filters
who talks about the same things
- Johannes Åman Pohjola2 talks
- Yong Kiam Tan7 talks
- Oskar Abrahamsson2 talks
- Thomas Sewell2 talks
- Scott Owens2 talks
- Peter Sewell14 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… | ||
| Brack: A Verified Compiler for Scheme via CakeML (Lightning Talk) | Scheme 2025 | 2025-10-16 |
Brack is a verified compiler for Scheme implemented in HOL4 that compiles a small subset (lambdas, lists, mutation) to ML and leans on CakeML to get down to… | ||
| Baking for Dafny: A CakeML Backend for Dafny | Dafny 2025 | 2025-01-19 |
A verified pipeline translates Dafny IR to CakeML by exporting the IR as S‑expressions, parsing and compiling inside HOL4, and extracting runnable CakeML code… | ||
| Much Still to Do in Compiler Verification (A Perspective from the CakeML Project) | PLDI 2024 | 2024-06-24 |
End-to-end verified compiler for an ML-like language (the CakeML stack) compiles functions in the proof assistant logic down to concrete machine bytes and… | ||
| They're the same picture: a software-verification flow adapted for hardware verification | PLARCH 2023 | 2023-06-17 |
Claims that the CakeML software-verification flow maps to hardware by replacing source functions with shallow-embedded Verilog, compiler correctness with a… | ||
| PureCake: A Verified Compiler for a Lazy Functional Language | PLDI 2023 | 2023-06-17 |
PureCake is a mechanically verified compiler built in HOL4 that translates a Haskell-like lazy language, PureLang, down to machine code by targeting and… | ||
| 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… | ||
| 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… | ||
| nothing matches | ||