~/talk

Modal FRP for all: Functional reactive programming without space leaks in Haskel...

Talkat ICFP 2023 · 2023-09-04..09-09· [functional-programming]
links:none on file
slides:none on file

A modal FRP language Ratus is implemented as a Haskell library plus a GHC plugin that enforces stricter typing: a later modality for time-shifted values and a box modality for stable (always-available) data. The compiler runs a multi-tick → single-tick transform, desugars to a strict core, and proves causality, absence of space leaks and productivity via a Lambda-tick core formalized in Coq. Ships with an FRP library and a Pong example; installable with cabal.

AI-written summary · about

  1. 0:00Intro
  2. 0:42Modal FRP
  3. 1:50Streams
  4. 3:34Model types
  5. 5:15Shallow embedding
  6. 7:23Ratus
  7. 8:40How Rus looks like
  8. 9:44How it works
  9. 12:47Memory leaks
  10. 15:44Stable types
  11. 18:24Pong game
  12. 19:34Implementation
  13. 22:52Met Theory
  14. 23:40Operations semantics
  15. 25:09Other resources
  16. 26:38Conclusion
~/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.