Updates
Visit our blog here.
For a roundup of the highlights every few months, read our newsletter [May, September].
Announcements, events, talks, and blog posts from FP Launchpad ↓
Upcoming
Recent
-
25-26 January 2027Event
FUN OCaml 2027
FP Launchpad hosts the first FUN OCaml in India: a day of talks and a keynote, followed by a day of workshops and collaborative hacking. The call for proposals is open through 30 September 2026.
-
2-3 October 2026
-
2-3 October 2026Event
SegFault 2026 Hackathon finale
In-person finale of an online hackathon on compilers and programming languages. FP Launchpad sponsors the Functional Programming theme.
-
1 Oct 2026Blogpost
FPL Reading: 1 October 2026
Kaustubh: Reflections from IndiaFOSS 2026. KC: Textbooks that run. Alina: Jigsawing an extended System-F calculus. Anil: .plan-26-39: End of my sabbatical, and I feeeel fine!, Mapping millions of little trees...
-
26 Sep 2026
-
26 Sep 2026
-
26 Sep 2026
-
26 Sep 2026
-
25-27 September 2026Event
IndiaFOSS 2026
Five talks and workshops from FP Launchpad members, across the main track and the Compilers, Programming Languages and Systems devroom.
-
25 September 2026Event
Workshop: Fun and Profit with OCaml
Hands-on OCaml workshop by Alina Banerjee, Smayan Agarwal, Kaustubh M and Vimala Soundarapandian, at IndiaFOSS 2026.
-
24 Sep 2026
-
18 Sep 2026
-
15 Sep 2026Blogpost
FPL Reading: 15 September 2026
Alina: The OxCaml Type system. Dhruv: How I reverse engineered an ASIC. Anil: .plan-26-37: The humans aren't dead, the humans are ahead, Hitting a NERVE with attacks on AI-powered brain-computer...
-
14 Sep 2026Blogpost
FP Launchpad update: research, teaching, and community
Six fellows have joined FP Launchpad. An update on our research, OCaml NPTEL course, environmental software projects, and upcoming events.
-
11 Sep 2026Seminar
Introduction to Modes in OxCaml, Part II
Abstract
OCaml's type system tells you the shape of a value, but not where it lives in memory, how many places still point to it, or whether it's safe to touch from another thread at the same time. This talk introduces OxCaml's mode system: a set of extra, independent checks the compiler layers on top of ordinary types to catch exactly these problems before the program ever runs, enabling faster memory management, safer mutation, and safe parallelism, all with zero runtime cost. We'll build up the intuition behind each of these checks from simple examples, and see where these checks apply and where they don't.
-
5 Sep 2026
-
1 Sep 2026Blogpost
FPL Reading: 1 September 2026
Anil: The 3rd Programming for the Planet 2026 videos are available, Celebrating a year of Tessera embeddings and releasing GeoTessera 0.10 and 2 more.
-
28 Aug 2026Seminar
Introduction to Modes in OxCaml, Part I
Abstract
OCaml's type system tells you the shape of a value, but not where it lives in memory, how many places still point to it, or whether it's safe to touch from another thread at the same time. This talk introduces OxCaml's mode system: a set of extra, independent checks the compiler layers on top of ordinary types to catch exactly these problems before the program ever runs, enabling faster memory management, safer mutation, and safe parallelism, all with zero runtime cost. We'll build up the intuition behind each of these checks from simple examples, and see where these checks apply and where they don't.
-
19 Aug 2026
-
15 Aug 2026Blogpost
FPL Reading: 15 August 2026
Harisankar: We are Problem Solvers. Anil: Improving local weather forecasts using Tessera embeddings, .plan-26-32: Finally a use for serverless and found the Forester for the trees and 3 more.
-
13 Aug 2026Seminar
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.
-
12 Aug 2026Seminar
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.
-
10 Aug 2026Blogpost
What the Interns Built This Summer
Our summer interns formalized school arithmetic in Lean, added biodiversity data to CoRE Stack, found and fixed a subtle bug in a verified CRDT, pushed OxCaml cryptography toward C speeds,...
-
6 Aug 2026Seminar
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.
-
1 Aug 2026Blogpost
FPL Reading: 1 August 2026
Alina: Putting Everything in Order. Anil: .plan-26-30: Bananas ripen, models open, and OxCaml releases, .plan-26-29: Perfect weather, imperfectly measured, precisely predicted.
-
31 Jul 2026Seminar
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.
-
30 Jul 2026Seminar
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 -
16–18 July 2026
-
15 Jul 2026Seminar
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 -
15 Jul 2026Blogpost
FPL Reading: 15 July 2026
Pranav: LeanLang Summer School - Days 3-5, LeanLang Summer School - Day 2 and 1 more. Harisankar: LLM Proposes, Lean Disposes: A Week at the LeanLang Summer School. Anil: .plan-26-27:...
-
14 Jul 2026Seminar
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 -
10 Jul 2026Seminar
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 -
6–10 July 2026
-
1 Jul 2026Blogpost
FPL Reading: 1 July 2026
Durwasa: GADTs in OCaml: The Type-Level Superpower Your Other Languages Wish They Had. Anil: .plan-26-26: Gelato, geospatial, and players of games, A scorching CNG London during Climate Action Week and...
-
15 Jun 2026Blogpost
FPL Reading: 15 June 2026
KC introduces an interactive O(x)Caml course book. Anil writes about TESSERA v1.1, Earth embeddings, CVPR, and self-hosting email.
-
1 Jun 2026Blogpost
FPL Reading: 1 June 2026
Pranav: The EuroSys 2026 Experience. Anil: .plan-26-22: From digital rewilding in Edinburgh to uring and Tessera hackery, Rewilding the Web: my workshop report from Edinburgh and 2 more.
-
15 May 2026Blogpost
FPL Reading: 15 May 2026
KC: Shrinking the OxCaml js_of_ocaml bundle: 285 MB to 4 MB, Capsules: compile-time lock discipline in OxCaml and 1 more. Durwasa: Prof CPR and the Resuscitation of Algorithmic Thinking, Soundness...
-
8 May 2026Blogpost
FP Launchpad members win prize at LeanLang Hackathon, IISc Bangalore
The LeanLang for Verified Autonomy Hackathon was a two-day event at IISc Bangalore organised by Prof. Siddharth Gadgil and Emergence AI, focused on applying Lean 4 to real-world multi-agent systems....
-
1 May 2026Blogpost
FPL Reading: 1 May 2026
KC: From Convergence to Confidence: Push-button verification for RDTs. Anil: Helping tropical forest protection keep up with a fast-changing world, .plan-26-17: Unwedging kernels, dogfood deployments, and managing beef leakage and...
-
27 Apr 2026
-
27 Apr 2026
-
13 April 2026Event
FP Launchpad Kickoff
Day-long conference with talks on hardware design, security, formal verification, compilers, programming languages, and AI-augmented software engineering.
-
10 April 2026Event
Talk by FPL Advisor Rishiyur Nikhil: Property Based Testing to Verify Pipelined CPU Hardware
Rishiyur S. Nikhil (Bluespec) on using Haskell QuickCheck to verify a 6-stage pipelined RISC-V CPU.
-
7 April 2026Event
Talk by FPL Advisor Nik Swamy: Agentic Proof-oriented Programming
Nik Swamy (Microsoft Research) on using AI agents with F* and Pulse to build programs with formal proofs of correctness.
-
1 Apr 2026Blogpost
Hello World
Welcome to the FP Launchpad blog. Follow this blog to get updates on what the centre is up to. Also check out our blogroll on the right for feeds of...
-
28-29 March 2026Event
CS Exebit 2026
Annual technical exhibition of the IIT Madras CS department. KC Sivaramakrishnan gave a talk on Functional Programming and OCaml, followed by a hands-on OCaml workshop. Pranav Ramesh led a workshop on Lean.
-
6 Mar 2026Announcement
Applications Open: Post-Baccalaureate Fellowship