~/talk

Better Defunctionalization through Lambda Set Specialization

on YouTube 23m
Talkat PLDI 2023 · 2023-06-17..06-21· [compilers-and-language-design]

speakers

name:William Brandon
links:none on file
name:Benjamin Driscoll
links:none on file
name:Frank Dai
links:none on file
name:Wilson Berkow
links:none on file
name:Mae Milano
website:https://www.cs.princeton.edu/~mpmilano/

resources

video:https://youtu.be/CYcf02fTE8E
slides:none on file

summary

Claims a compiler pass called Lambda set specialization that turns defunctionalization into type monomorphization, implemented as a polymorphic internal type system with a tractable inference algorithm and mechanized soundness and completeness proofs in Isabelle/HOL. A preprocessing pass targets MLton (Standard ML), OCaml, and the Morphic compiler; it generates specialized first‑order code, yields speedups (average 1.9x MLton, 3.45x OCaml, up to 78.93x on Morphic, best cases ~6.85x/3.45x/78.93x), and changes binaries by at most 35%.

AI-written summary · about

chapters (12)

  1. 0:00Lambda set specialization intro
  2. 1:47Lambdas expensive in functional langs
  3. 3:11Defunctionalization goals
  4. 6:36Prior techniques and limits
  5. 9:25Lambda set specialization approach
  6. 13:18Implementation results and gains
  7. 15:25Lessons from LSS in practice
  8. 16:29Summary and future of LSS
  9. 17:10Q&A on type-preserving compilers
  10. 18:55Comparison with continuation passing style
  11. 20:39LSS analysis complexity
  12. 22:46Closing remarks

related talks

~/search
type to search 6,249 conferences, 138,987 speakers and 185,172 talks
~/help
cmdctrl k
search every conference, speaker and series
/
focus the filter search
h
home
c
conferences
s
speakers
e
series
t
light / dark — the status bar button does the same
?
this help
esc
close this, then clear every filter — or just the search, while you are typing in it

Ignored while you are typing. Pages without a filter rail have no search to focus.