Talks
Talks given by FP Launchpad members on their research and projects, at internal and external venues.
External
Internal
Sound and Optimal Stateless Model Checking for Operation Based CRDTs
Repo:
model_checking_rdts
Introduction to Separation Logic :: Part II
Abstract >
A gentle introduction to the core ideas behind Separation Logic and the Iris framework. Covers how assertions about memory differ from classical Hoare Logic, the separating conjunction (*) and the frame rule, and how these concepts simplify correctness proofs for programs operating on linked data structures.
Neurosymbolic Planner Synthesis Incorporating Specification Closeness
Abstract >
In robotics and related applications, specifications used to define objectives, as well as safety or liveness constraints, may result in infeasible solutions because of characteristics of the underlying controller. The current state of the art places the burden on the developer to reassess objectives. In contrast to this cumbersome process, we consider an alternative formulation in this project: by translating specifications into a suitable embedding space, we can effectively explore a family of close specifications, separated by some epsilon in this space, using these as potential alternatives. This idea is broadly related to the notion of robustness in learning but framed at the level of logic, rather than observations.
Introduction to Separation Logic
Abstract >
An introduction to core concepts of Separation Logic and the Iris framework. Covers how memory assertions differ from classical Hoare Logic, the separating conjunction operator and frame rule, and how these principles streamline correctness proofs for programs working with linked data structures.
What is in an Inductive Type? A Look in with Lean
Abstract >
Inductive types play a central role in functional programming, enabling developers to construct types with multiple constructors. This talk explores how these constructs facilitate recursive function definitions while addressing termination verification challenges, and examines their application to mathematical induction principles commonly used in formal proofs. Using Lean as the primary tool, the session investigates the fundamental properties and practical implications of inductive types in theorem proving.
Convergence is Not Correctness: Verifying a Tombstone-free Sequence MRDT in Lean 4
Abstract >
A collaborative editor cannot describe an edit by the offset where it lands, since a concurrent edit moves every offset after it. RGA solves this by naming characters, but keeps every deleted character forever as a tombstone, so state grows with the number of edits rather than with the size of the document. This talk reports an attempt to remove tombstones: a tombstone-free RGA as a Mergeable Replicated Data Type, verified in Lean 4 using Sal, a port of the F* framework Neem.
Repo:
sal
Making Sense of eBPF
Abstract >
An exploration of the eBPF subsystem of the Linux kernel, starting with historical context and the programming languages available for eBPF development. The core of the talk covers the BPF instruction set architecture, its type system, and the verification step, alongside the kernel's JIT compiler backend, concluding with the challenges the current BPF model poses.
Repo:
ebpf_gen
Long Division Has a Proof: Teaching Formal Verification Through School Arithmetic
Abstract >
Formal verification, the practice of proving that a program is correct for every possible input, not merely those that have been tested, is widely regarded as specialist work. This talk argues that this reputation is largely a teaching problem. Using familiar pen-and-paper arithmetic algorithms as case studies, it shows that the central ideas of formal verification (specifications, loop invariants, induction, and termination) are already latent in these algorithms and emerge naturally once we ask why they work. The accompanying open-access book, Learn2Lean, makes this concrete: each chapter implements one algorithm in Lean 4, proves it correct, and pairs the proof with step-by-step visualizations and an in-browser exercise checker that compiles real Lean code against student submissions.
Repo:
Learn2Lean
Benchmarking on Modern Hardware
Abstract >
As technology evolves, attributing performance improvements becomes harder: gains can come from code changes, caching, or garbage collection, and it is not always obvious which. This talk looks at what to watch out for when benchmarking, with scenarios drawn from real-world OCaml optimization work, and lays out ideas, old and new, for a benchmark suite that supports cutting-edge research while preserving legacy code performance and production stability.
Repo:
retro-httpaf-bench