Pipit: Reactive Systems in F★ for Safety-Critical Control Systems

Explore a conference talk introducing Pipit, a small reactive language embedded in F★ designed for verifying control systems and executing them in real-time. Discover how Pipit includes a verified translation to transition systems and leverages F★'s existing proof automation to automatically prove certain safety properties using k-induction. Learn about Pipit's ability to generate imperative code in a subset of F★ suitable for compilation and real-time execution on embedded devices. Understand the ongoing work on proving that the imperative code preserves semantics, while noting that the translation to imperative code preserves types by construction. Gain insights into the potential applications of Pipit in implementing and verifying safety-critical control systems.

[TyDe'23] Pipit: Reactive Systems in F★ (Extended Abstract)