F* PoP Up Seminar

Time: Next event on Tuesday, November 7, 2023 (830am Pacific Standard Time)
Speaker: Sheera Shamsu on Mechanised Verification of an OCaml-style Garbage Collector
Location: Zoom
Youtube channel: YouTube
Join fstar-mailing-list@googlegroups.com for future announcements.

Overview

F* is a Proof-oriented Programming Language that allows writing programs and proofs about them within a single framework. Software components developed and proven correct and secure in F* have been deployed in various production systems, including Microsoft Windows Hyper-V, Microsoft Azure, the Linux kernel, and Firefox.

The F* PoP Up Seminar is a monthly event aimed at bringing together the F* community. It is a discussions-oriented, informal seminar where the attendees may:

Learn about each other’s F* libraries and tools
Share their experiences on common F* proof patterns and styles that work well and, equally importantly, that may not
Present their F* development and get feedback from the community
Discuss F* future directions, and upcoming features and libraries

Each event in the seminar will be at most one-hour long, featuring one or more presenters who will lead the discussion. The sessions will be interactive, may involve code walkthroughs, deep-dive discussions, live coding, detailed proof debugging, and maybe even some slides!

To propose a talk, send an email to the Google group with the following details:

Title
A small abstract: what is the talk about and what would you like to get out of it (e.g. get feedback on a library I am developing, get feedback on a proof-style that I found cumbersome, tell the community about my experience with what worked and what didn’t)
How much time you think you’ll need
Your availability

We look forward to your proposals!

Schedule

Date	Speaker(s)	Topic
November 7, 2023 (830am PST)	Sheera Shamsu	Mechanised Verification of an OCaml-style Garbage Collector Programming languages with managed runtimes often provide memory safety with the help of a garbage collector (GC). GCs are often implemented in an unsafe language like C and utilise low-level memory operations. Bugs in the GC implementation affects the memory safety guarantees of the managed language. In this work, we present a specification and verification framework for GCs operating over OCaml-style objects. Unlike prior work, our correctness conditions are based on graph reachability, which permits evolution of the GC without having to rewrite the core safety specifications. Our framework is developed in F, a proof-oriented solver-aided programming language, and its subset Low, which facilitates extraction of verified C code. Using this framework, we have verified a stop-the-world mark and sweep GC which is compatible with OCaml. Our experimental results illustrates that the extracted verified code performs on par with a handwritten GC implementation.
September 19, 2023 (830am PST)	Subhajit Roy	The Lazy Professor's Route to Teaching Programming Language Semantics a.k.a. A Theorem Proving Approach to PL Semantics The talk will unfold the story of a lazy professor who felt that using theorem provers is an "easy" shortcut to messy proofs while teaching programming languages theory. We will discuss his experience of using this methodology (and the story of distressed students) in an ACM summer school on programming languages. Once the program and its semantics are encoded in any of the different styles—operational, denotational, or axiomatic, powerful proof assistants like F* can prove exciting language features with minimal human assistance. The hope is that teaching programming languages via proof assistants will not only provide a more concrete understanding of this topic but also prepare future programming language researchers to use theorem provers as fundamental tools in their research and not as an afterthought. Well, although the methodology was born out of the professor's attempt at saving face after a heavy dose of procrastination, it opens up interesting questions on if undergraduate students are ready enough to date theorem provers. Related paper
July 25, 2023 (830am PDT)	Cezar Andrici	Securing Verified IO Programs Against Unverified Code in F* YouTube recording of the talk, Paper, Code.
June 27, 2023 (830am PDT)	Abhishek Bichhawat	DY*: A Modular Symbolic Verification Framework for Executable Cryptographic Protocol Code (related paper, from Euro S&P 2021, YouTube)
May 2, 2023 (5am PDT)	Amos Robinson	Pipit: early work verifying reactive control systems in F* (related blog post, YouTube
December 6, 2022	Nik Swamy	Understanding how F* uses Z3 (YouTube, Chapter)
October 11, 2022	Guido Martinez	Tactics and Metaprogramming (YouTube, Demo code samples, Draft chapter)
September 6, 2022	Jay Bosamiya	vWasm: Verified Software Sandboxing using F* (related paper, from USENIX Security 2022), YouTube
August 9, 2022	Alex Rozanov	Abstract Algebra in F* (Slides, YouTube)
July 12, 2022	Vimala Soundarapandian	Replicated Data Types (YouTube, Code)
July 12, 2022	Lucas Franceschino	A REPL for Tactics in F* (YouTube)

Organizers

Lucas Franceschino (INRIA)
Joshua Gancher (CMU)
Aseem Rastogi (MSR India)
Nikhil Swamy (MSR Redmond)
Théo Winterhalter (MPI-SP)