~/talk

A Pretty Expressive Printer

on YouTube 17m
Talkat OOPSLA 2023 · 2023-10-23..10-27· [compilers-and-language-design]

speakers

name:Sorawee Porncharoenwase
links:none on file
name:Justin Pombrio
links:none on file
name:Emina Torlak
links:none on file

resources

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

summary

Claims a new printer Πe that is strictly more expressive than prior pretty printers, provably minimizes a user-chosen optimality objective via a Cost Factory, and has better worst‑case time complexity than many existing systems. The algorithm is formulated as dynamic programming, uses memoization and a low‑dimension parallel frontier data structure, is verified in the Lean theorem prover for validity and optimality, and is implemented as PrettyExpressive, which evaluates competitively and already underpins a Racket code formatter.

AI-written summary · about

chapters (8)

  1. 0:00Introduction
  2. 2:11Traditional vs arbitrary printers
  3. 3:55Expressiveness versus performance
  4. 7:08Sigma e printing language
  5. 9:14Optimality with dynamic programming
  6. 11:01Memoization for performance
  7. 12:44Evaluation results
  8. 14:34Q&A

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.