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.


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:

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:

We look forward to your proposals!


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)