 |
Our First Newsletter
May 2026
|
|
Education
NPTEL Course: Functional Programming with OCaml
KC Sivaramakrishnan is offering Functional Programming with OCaml on NPTEL in the July 2026 semester. Enrollment is open now, free for all.
The course comes with an interactive book where you can run OCaml directly in your browser. The goal: make 0-to-OCaml take 0 steps, including using OCaml's platform tools: no installation, no setup, just open and start coding.
Technical note
Your OCaml program runs in a bytecode interpreter, on an emulated x86 CPU, JIT-compiled to Wasm, running in your browser, JIT-compiled to run on your local machine.
The first 8 modules are stable; the rest is being built in the open.
Register on NPTEL
Interactive course book
|
Award
LeanLang Hackathon, IISc Bangalore
Vimala Soundarapandian and Durwasa Chakraborty competed as team sambar&Soundness at the LeanLang for Verified Autonomy Hackathon at IISc Bangalore, taking 2nd prize for QueryBridge, a Lean 4 tool that formally verifies query translation between JSON and SQL.
Blog post
|
Research
PaPoC 2026: Keynote and Paper
KC Sivaramakrishnan gave an invited keynote, "From Convergence to Confidence: Push-Button Verification for Replicated Data Types", at PaPoC 2026 (co-located with EuroSys, Edinburgh). The talk argues that convergence alone is not enough to verify replicated data types, and introduces Sal, a Lean 4-based framework using Small Proof-Oriented Tests (SPOTs) to close the gap.
Pranav Ramesh and Vimala Soundarapandian co-authored the paper "Sal: Multi-modal Verification of Replicated Data Types", presented at the same workshop.
Keynote slides
Blog post and explainer
Paper
Interactive playground
PaPoC 2026
Pranav's writeup
|
Security
FIDES at AsiaCCS 2026
Sai Venkata Krishnan and collaborators published "FIDES: End-to-end Compartments for Mixed-language Systems" at AsiaCCS 2026. FIDES uses hardware-assisted compartments on the Shakti RISC-V platform to isolate components in mixed-language programs, limiting the blast radius of bugs across language boundaries.
|
Event
CS Exebit 2026, IIT Madras
FP Launchpad was a Gold Sponsor of CS Exebit 2026, the annual technical exhibition of the IIT Madras CS department, held March 28-29. KC Sivaramakrishnan gave a talk on Functional Programming and OCaml, followed by a hands-on OCaml workshop open to all skill levels. Pranav Ramesh led a separate workshop on Lean.
CS Exebit 2026
|
Event
Kickoff Event, IIT Madras
FP Launchpad launched at IIT Madras on April 13, 2026, with a full-day programme spanning hardware design, security, formal verification, compilers, and AI-assisted software engineering. Speakers included Rishiyur S. Nikhil (Bluespec), Chester Rebeiro (IIT Madras), Krishnan Raghavan (Pramaana Labs), Manas Thakur (IIT Bombay), Anil Madhavapeddy (Cambridge), Yaron Minsky (Jane Street), Shriram Krishnamurthi (Brown University), and Ilya Sergey (NUS). All 10 talks are on YouTube.
Browse the talks
Event page
|
Talks
Seminars at IIT Madras
In April, we hosted two seminars at SSB 334, IIT Madras:
|
Nik Swamy
Microsoft Research · April 7, 2026
Agentic Proof-oriented Programming
On using AI agents with F* and Pulse to produce verified code at scale, including a port of a verified garbage collector.
|
|
Rishiyur S. Nikhil
Bluespec · April 10, 2026
Property Based Testing to Verify Pipelined CPU Hardware
Applying QuickCheck to hardware verification of a 6-stage pipelined RISC-V CPU using TestRIG and the Sail ISA formal model.
|
|
|
New Faces, and Fond Farewells
This month, FP Launchpad welcomes its first cohort of Post-Baccalaureate Fellows alongside a group of summer interns. At the same time, several BTech and MTech students who have been part of the lab are graduating and moving on to their next chapters. We wish them well.
The next newsletter will introduce the new cohort and what they are working on.
If you are interested in working with us, as a collaborator, visitor, or future fellow, write to careers@fplaunchpad.org.
|
|
|
|