Kacper F. Korban
PhD student, SYSTEMF, EPFL
I am a PhD student at SYSTEMF@EPFL, supervised by Clément Pit-Claudel. My research is focused on compilers (especially verified ones), programming languages and formal verification. I am also interested in developer tooling, types, and software engineering in general.
E-mail · GitHub · Google Scholar · ORCID · CV
Selected work
- ESOP 2024
Verified Inlining and Specialisation for PureCake
Abstract
Inlining is a crucial optimisation for functional languages. We implemented and verified function inlining and loop specialisation for PureCake, a verified compiler for a Haskell-like, purely functional, lazy language. A novel part of our formalisation justifies inlining by pushing and pulling let bindings. The work was mechanised in HOL4.
- POPL SRC 2026