~/talk

A Type-Safe Structure Editor Calculus + Strictly Capturing Non-Strict Closures

on YouTube 01h 00m
Talkat PEPM 2021 · 2021-01-18..01-19· [developer-experience]

speakers

name:Christian Godiksen
links:none on file
name:Thomas Herrmann
links:none on file
name:Hans Hüttel
links:none on file
name:Mikkel Korup Lauridsen
links:none on file
name:Iman Owliaie
links:none on file
name:Zachary Sullivan
links:none on file
name:Paul Downen
website:https://www.pauldownen.com/
name:Zena M. Ariola
links:none on file

resources

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

summary

Two short papers: one builds a type-safe editor calculus with cursors, holes, breakpoints and a small-step semantics and gives a behavioral type system (path-indexed contexts, a linear-style split for sequencing) that proves subject reduction and that well-typed edit sequences cannot produce ill-typed ASTs; the calculus is expressive enough to be Turing-complete and is being pushed toward a structure-oriented IDE. The other formalizes closure conversion for non-strict languages, shows correctness requires a strict target (or heap+memo for call-by-need), proposes partial closure conversion for lazy IRs, proves many preservation theorems and leaves a future-heap lemma for full call-by-need completeness.

AI-written summary · about

chapters (21)

  1. 0:00Introduction
  2. 0:23Type-safe structure editor calculus
  3. 2:26Editor calculus with cursors
  4. 6:20Spatial logic in editor
  5. 7:48Editor expressions syntax
  6. 12:05Type safety in edit actions
  7. 18:06Type system guarantees
  8. 19:07Results and future work
  9. 21:14Q&A on editor calculus
  10. 28:37Strictly capturing non-strict closures
  11. 30:07Closures in strict languages
  12. 31:57Non-strict language challenges
  13. 36:17Call-by-name closure conversion
  14. 40:13Non-strict data limitations
  15. 42:42Correctness of call-by-name conversion
  16. 44:28Target language requirements
  17. 46:17Call-by-need closure conversion
  18. 51:23Partial closure conversion
  19. 53:59Summary and future directions
  20. 55:06Q&A on closure conversion
  21. 59:05Session wrap-up

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.