Pipit: Reactive Systems in F★ (Extended Abstract)
summary
Pipit is a small embedded DSL in F★ that implements reactive streams with Follow by delays and guarded recursion, provides a verified translation to transition systems, and uses F★ proof automation to discharge safety properties by k‑induction. It can emit imperative code in a subset of F★ for microcontrollers and already runs on real devices, but only half the semantic refinement proof is done, abstraction support is minimal, common‑subexpression elimination is needed before transition translation, and clocks and richer types remain unimplemented.
AI-written summary · about
chapters (10)
- 0:00Reactive systems in F*
- 0:45Reactive systems challenges
- 2:55C problematic for verified systems
- 4:01Lifting logic to streaming
- 6:10Driver in F* with DSL
- 7:16Correctness properties for driver
- 9:45Proving via transition systems
- 10:50Embedded DSL in F*
- 12:35Limitations and future work
- 14:21Q&A
related talks
21mSecurely Compiling F* Programs With IO and Then Linking Them Against Weakly-Typ...
26mFusing Session-Typed Concurrent Programming into Functional Programming
16mTowards formally secure compilation of verified F* programs against unverified ML(…)
21mMaking Concurrent Hardware Verification Sequential
01h 02mPolyglot Programming through Foreign Function Interfaces
01h 00mBuilding DSLs on Top of KernelF
41mAn Introduction to Functional Imperative Programming in Flix
41mTowards language support for distributed systems