ICFP 2023
Mon 4 - Sat 9 September 2023 Seattle, Washington, United States
Mon 4 Sep 2023 17:07 - 17:30 at St Helens - TyDe: Type-Driven Runtimes Chair(s): Ningning Xie

Reactive languages such as Lustre and Scade are used to implement safety-critical control systems; proving such programs correct and having the proved properties apply to the compiled code is therefore equally critical. We introduce Pipit, a small reactive language embedded in F★, designed for verifying control systems and executing them in real-time. Pipit includes a verified translation to transition systems; by reusing F★’s existing proof automation, certain safety properties can be automatically proved by k-induction on the transition system. Pipit can also generate imperative code in a subset of F★ which is suitable for compilation and real-time execution on embedded devices. This translation to imperative code preserves types by construction; the proof that the imperative code preserves semantics is ongoing.

Mon 4 Sep

Displayed time zone: Pacific Time (US & Canada) change

16:00 - 17:30
TyDe: Type-Driven RuntimesTyDe at St Helens
Chair(s): Ningning Xie University of Toronto
16:00
22m
Talk
Semantic Encapsulation using Linking Types
TyDe
Daniel Patterson Northeastern University, Andrew Wagner Northeastern University, Amal Ahmed Northeastern University, USA
DOI
16:22
22m
Talk
Towards Tagless Interpretation of Stratified System F (Extended Abstract)
TyDe
Peter Thiemann University of Freiburg, Germany, Marius Weidner University of Freiburg
File Attached
16:45
22m
Talk
Types as First-Class Values in Fuzion (Extended Abstract)
TyDe
Fridtjof Siebert Tokiwa Software GmbH
File Attached
17:07
22m
Talk
Pipit: Reactive Systems in F★ (Extended Abstract)
TyDe
Amos Robinson Australian National University, Australia, Alex Potanin Australian National University
File Attached