Nexct FP Syd: 27 March

[Jost Berthold]

FP Syd is on again next Wednesday, 27 March. Please RSVP on meetup.com (or let the organisers know) if you'd like to attend.We have one full-size talk this time, so we can accommodate 1-2 lightning talks, too. As usual, doors open at 6pm for the talks to start around 6:45.Amos Robinson - Pipit on the Post: proving pre- and post-conditions of reactive systems
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 executable code in a subset of F* which is suitable for compilation and real-time execution on embedded devices. The executable code is deterministic and total and preserves the semantics of the original program. This talk is based on a paper currently in submission.And once again: We are still in need of speakers to fill our roster for 2024.
Please consider presenting something Functional Programming related, get in touch with the organisers and/or open a PR on http://github.com/fp-syd/meetings.