Compilers

Papers on compiler design and verification from POPL, PLDI, OOPSLA, ECOOP, and ICFP.

---

2025

• Compiling with Generating Functions — ICFP 2025
  Using generating functions as a mathematical basis for compiler transformations.

• Correctness Meets Performance: From Agda to Futhark — ICFP 2025
  Methodology for extracting verified GPU programs from Agda specifications.

• Environment-Sharing Analysis and Caller-Provided Environments for Higher-Order Languages — ICFP 2025
  Analysis detecting when closures can share environments, reducing memory use.

• Verified Compilation of a Dependently Typed Language — PLDI 2025
  Mechanized (Coq) compiler correctness for dependent type theory, including proof erasure and code generation.