# The FP Launchpad takes off at IIT Madras *2026-04-13 — note* This week I hopped over to Chennai for the launch of the [FP Launchpad](https://fplaunchpad.org), a brand new Centre for Functional Systems Research and Education at IIT Madras. It's run by my long-time collaborator and friend [KC Sivaramakrishnan](https://kcsrk.info), who was a postdoc in my [OCaml Labs](https://anil.recoil.org/projects/ocamllabs) group in Cambridge before moving to IIT Madras as a professor. I eagerly flew in for a couple of days accompanied by [Ryan Gibb](https://ryan.freumh.org) to soak in the atmosphere and start building stronger links between Cambridge and Chennai.

The FPL's mission is to build "[efficient, reliable and trustworthy software with mathematical guardrails](https://fplaunchpad.org/)", good timing given the firehose of AI-generated code we are all [drinking](https://anil.recoil.org/notes/internet-immune-system) from these days. Jane Street is the founding donor and the FPL advisory board has a nice international flavour with folk from Purdue, UCSD, Brown, Cambridge (me) and Microsoft Research. The centre's first big programme is a [post-bacc fellowship](https://fplaunchpad.org/2026/03/06/applications-open-post-bacc-fellowship.html): a 2 year fully funded position with travel support and the exit path is whatever works best for the student (academia, industry, or both). The deadline for the first batch is the 20th April, so do [apply](https://docs.google.com/forms/d/e/1FAIpQLSdhS9b4vX1u7T1pAFhXc4ZADJXtVIFkHgUvjZOW1K9q9L9I9g/viewform) if you know anyone who would be a good fit\! ## On campus at IIT-M Ahead of the meeting on Monday, I spent a day hanging out on campus and getting my bearings. This is easily the most beautiful university area I've seen (except for Cambridge of course): banyan trees with aerial roots draped everywhere, flying fox bats heading out at dusk, and deer wandering around between buildings. I [noted earlier](https://anil.recoil.org/notes/2026w15) how much I enjoyed the IIT-M coffee shop near the student quarters to run into IIT-M PhD students and hear about life on the inside. There's also a really nice [Heritage centre](https://www.iitm.ac.in/the-institute/about-iit-madras/heritage-centre) on the campus where they explain how the IIT was set up with the assistance of the German government.

The FP Launchpad brings functional programming up front to IIT-M!

I'm competing with Shriram for 'most out of date' picture here

On Monday morning I arrived at the [IC\&SR](https://icandsr.iitm.ac.in/) building and it was immediately obvious this was a quintessentially Indian affair: heaps of fresh flowers and a giant arch proclaiming the arrival of the FPL\! KC's logo for the centre is well worth staring at: the lines form a camel, there's a lambda in the middle, and it spells out an 'M' (for Mirage or Madras, take your pick, and probably more besides). The speaker list was prominently signposted, and there was delicious [Indian filter coffee](https://en.wikipedia.org/wiki/Indian_filter_coffee) available to get us going.

The room itself where the conference was held was extremely modern; a giant LCD screen, full AC for a hot day, and excellent support for remote speakers with sound capture throughout the auditorium. ## Opening talks The centre head, [KC Sivaramakrishnan](https://kcsrk.info), opened with the motivation: software is everywhere, but much of it is fragile and insecure, and meanwhile AI agents are writing more of it at scale than ever before. India is a great place to drive this work since it produces [more software engineers than anywhere else](https://en.wikipedia.org/wiki/Software_engineering_demographics#India), but the foundational PL pieces are mostly being built elsewhere right now. The FPL aims to change that and is organised around three pillars: research/development, education/training, and systems/community with each one feeding the others.

KC opens up proceedings with an explanation of how FPL works

KC also noted that what used to take a year of work can now happen in mere moments with AI assistance, but at the same time nothing replaces human intuition for the elegant software abstractions that FP typifies. With the world changing due to AI, we need to figure out how to preserve the key intuitive leaps that the next generation of practitioners can learn to ensure code isn't just AI slop. In a nod to how seriously IIT-M is taking the FPL, the institute's director [Kamakoti](https://heritage.iitm.ac.in/directors-gallery/prof-v-kamakoti) also gave an address. His observation was that the state of software development is becoming increasingly decoupled from verification and performance. When these are merged into a whole system, there is no room for cross-cutting optimisations and bugs are increasingly cross-functional. He pointed at [Shakti](https://shakti.org.in/), the RISC-V processor line that has [made it into space](https://www.youtube.com/watch?v=HjYdUx9LPTA) (which [Thomas Gazagnaire](https://github.com/samoht) will [like](https://gazagnaire.org/blog/2026-04-07-ssa.html)) as proof that India can build a full hardware/software systems stack from scratch that is also sovereign and correct by construction. He was also clear that this isn't about functional programming for toy programs: there are multiple large projects underway at the centre, and that kind of scale is necessary to properly test the concepts.

A giant Ron Minsky appears in the auditorium

We also had a donor address from Jane Street in the form of [Yaron Minsky](https://github.com/yminsky), beaming in super early in his morning from Pittsburgh where he was due to give another talk at CMU later in the day! Yaron described the excitement at Jane Street about closing the feedback loop between production deployments of their compiler (deployed multiple times a month into production trading) and speeding up the research loop by writing papers on experimental extensions, and also teaching the new concepts such as modes (as we did with the [OxCaml tutorial](https://anil.recoil.org/notes/icfp25-oxcaml) at ICFP 2025 recently). This is a pretty unique situation as far as I'm aware in PL research. In my [own](https://anil.recoil.org/notes/bushel-lives) [use](https://anil.recoil.org/projects/oxcaml), I've never had a single binary crash attributed to a compiler bug in OxCaml itself, so it's a surprisingly rock-solid compiler. There are plenty of bugs in the experimental type system extensions of course, but those are safely gated behind language keywords so you know when you're using them. It's genuinely very fun using a fast-moving but stable compiler that can _also_ incorporate bleeding edge research within [weeks](https://thicket.dev) of the idea being written down. ## Research talks We then moved onto a programme of fast-paced research talks. I'll skim each one to give you a sense of what the FPL is interested in pursuing. ### Rishiyur Nikhil on Bluespec Rishiyur Nikhil kicked off with a grand unified pitch that "hardware is software, and software is hardware". [Bluespec](https://www.bluespec.com/) is his long-running project to show that both disciplines are really "designing on the same planet", and to remove the schism by treating hardware design as a functional programming exercise. Concurrent atomic transactions are the core around which Bluespec works, and this scales up to complex processors like Shakti or the CHERI CPU [my Cambridge colleagues build](https://www.cl.cam.ac.uk/research/security/ctsrd/cheri/). He walked through property-based testing via [QuickCheck in Bluespec](https://fplaunchpad.org/2026/04/09/rishiyur-nikhil-property-based-testing-pipelined-cpu.html), and then presented a test rig that repackages QuickCheck to compare implementations against the official RISC-V formal spec written in [Sail](https://www.cl.cam.ac.uk/~pes20/sail/) (another Cambridge project!). I like his term "algoltecture" to describe algorithmic implementations in circuits; e.g. you can have a merge sort interface with ten different mergesorts in hardware, each conforming to the same spec but making different area/timing tradeoffs. Picking between them is a balancing act between the hardware requirements while staying in the right algorithmic design space. The audience Q\&A revealed something I'd been curious about as well: the Verilog output from Bluespec is actually quite readable. Register instantiation inside the generated Verilog is tidy, although (unsurprisingly) the control logic for timing is where the complexity ends up. I remember chatting to [Andy Ray](https://github.com/andrewray) years ago in 2015 about how difficult the [control logic synthesis](https://doi.org/10.1145/3622781.3674170) process is to automate across arbitrary circuit descriptions.

RS Nikhil explaining the joys of Bluespec for hardware design

### Chester Rebeiro on trusted hardware Chester Rebeiro spoke on "trusted hardware for security-critical software", describing the large attack surface via Trusted Execution Environments and how to shrink it so sensitive memory regions are not accessible even from ring 0. When protected assets need to be touched the processor execution transitions into a secure mode, and his research focuses on making this switching efficient enough that developers are happy to use it on realistic workloads. I've worked on [DIFC for TEEs](https://anil.recoil.org/projects/difc-tee) before, so this talk was of interest\! He presented two approaches that are both built on the Shakti RISC-V platform. The first is [TESLA](https://doi.org/10.46586/tches.v2025.i4.899-924), a lightweight TEE that demonstrates how minimal hardware extensions can enforce confidentiality/integrity in the presence of a malicious OS while also retaining low overhead. This is done especially for legacy embedded workloads that can't easily be rewritten. His approach used encrypted parameter passing to avoid deep copies, and even worked at a sub-cacheline level (which surprised me; I must read the paper to get more details on how this bit-level access can be fast enough to be practical). The second is [FIDES](https://kcsrk.info/papers/fides_asiaccs_2026.pdf) which attacks intra-application security via fine-grained hardware-assisted compartments for mixed-language programs (like OCaml and C, so relevant to MirageOS!). FIDES provides strong isolation between components written in different languages so that the blast radius of an exploit stays scoped, but also supports fast function calls within a typesafe process (e.g. the OCaml heap). This gives an incentive to write secure code, as it'll perform better than mixing in with C that requires the hardware enforced protection checks. - [TESLA: Trusted Execution Support for Legacy Embedded Applications](https://doi.org/10.46586/tches.v2025.i4.899-924) - [FIDES: End-to-end Compartments for Mixed-language Systems](https://kcsrk.info/papers/fides_asiaccs_2026.pdf)

Chester Rebeiro describes TESLA and FIDES

### Krishnan Raghavan on verifiable governance Krishnan Raghavan gave one of my favourite talks of the day on combining LLMs with Lean to build verifiably correct representations of legal statutes like Indian tax laws. When governments deploy AI in tax administration, for regulatory compliance, or any citizen-facing legal systems, the correctness is a constitutional expectation around here. This obviously won't work with today's black box LLMs, which makes them fundamentally unsuitable as the sole basis for governance infrastructure unless some other verification mechanism is available. The LegalLean approach establishes a correspondence between (natural language) law and (machine-checkable) Lean code via a DSL they have designed. This enables provable correctness of rule application, automatic contradiction detection across large statute bodies (of tax law to start with), and fully deterministic outputs that can be audited. The results presented come from formalising provisions of the [Indian Income Tax Act 2025](https://www.incometaxindia.gov.in/income-tax-act-2025), and the demonstration in the talk could spot contradictions in real time as the DSL typechecked in the browser. I liked how the approach combines [Catala](https://catala-lang.org/) (the legal DSL coming out of the French tax code formalisation) with LLM-assisted translation into Lean for verification. It feels very pragmatic, and I had a long chat with Krishnan afterwards about whether the same toolchain could be pointed at causal synthesis from the [Conservation Evidence](https://anil.recoil.org/projects/ce) literature database we've built at Cambridge. We also need to spot contradictions between studies and their underlying interventions, or test hypotheses. Their startup is called [Pramaana Labs](https://www.pramaanalabs.ai/), and I imagine they'll connect with Sarvam (the India-specialised LLM trainers I met at the [AI Impact Summit](https://anil.recoil.org/notes/india-ai-summit) earlier this year).

Krishnan Raghavan on Verified AI for Indian governance infrastructure

### Manas Thakur on precise analysis for efficient JIT optimisation After the lunch break, Manas Thakur from IIT Bombay kicked us off with a great talk on combining precise program analysis with just-in-time compilation in the JVM (after making apologies for not being 'functional' enough). Conventional wisdom is that precise static analysis is too expensive for JIT settings where the compiler has to keep things realtime (like in a browser). Manas instead uses precise analysis to unlock memory optimisations that a lighter-weight analysis would have to omit. His recent work [CoSSJIT](https://dl.acm.org/doi/10.1145/3763149) uses static analysis to guide optimistic stack allocation of objects, backed by a dynamic heapification that restores correctness whenever the runtime dynamism of the JVM violates the assumptions. Interestingly, he also showed how speculative JIT information can feed _back_ into the static analysis to improve its precision, so the AOT and JIT end up benefiting each other. This isn't something that [OxCaml](https://anil.recoil.org/projects/oxcaml) does at all at the moment I think.

Manas Thakur shows how precise static analysis pays off inside a JIT

### Ilya Sergey on an experiment in AI-Assisted Metatheory

Meeting Ilya over at the IIT-M Bose-Einstein guest house

Ilya Sergey then took the stage to describe a wild AI vibe-proving journey he has been on for the past few months, which was eerily similar to my more [systems oriented explorations](https://anil.recoil.org/notes/aoah-2025) last Christmas. He described the mechanised metatheory and soundness proof for a regex-based borrow checker for Move, a smart contract language. The type system tracks aliasing as regular expressions over field paths, using [Brzozowski derivatives](https://en.wikipedia.org/wiki/Brzozowski_derivative) for field borrows and Kleene stars for unbounded aliasing from function calls and loops. In this model, write safety in the presence of aliasing reduces to a simple decidable regex emptiness check. Very cool\! The remarkable part though, was the process. Ilya drove Claude Code over a month (in the background) to achieve full mechanisation of Move in ~39K LOC of Lean 4 code, tested against the production Move compiler for compatibility, and usable as a reference implementation. His vision is that AI-assisted formalisation of realistic programming languages shifts the bottleneck from _writing_ proofs to _designing_ invariants, which makes machine-checked mechanisation a practical tool for iterative prototyping of correct-by-construction type systems. When combined with [Nik Swamy's recent results](https://fplaunchpad.org/2026/04/03/nik-swamy-agentic-proof-oriented-programming.html) on agentic proof-oriented programming in F\*/Pulse (covered in [this week's weekly](https://anil.recoil.org/notes/2026w15)), this is starting to look like an inflection point for mechanised semantics just like [in mathematics](https://www.quantamagazine.org/the-ai-revolution-in-math-has-arrived-20260413/). I spent a lot of time chatting to Ilya during and after the event, and he's finally convinced me to give Lean a serious try. [Ryan Gibb](https://ryan.freumh.org) has already been using it over the past month to mechanise our [package calculus](https://anil.recoil.org/papers/2026-package-calculus) work, so it's high time I had a go myself. As a first project I'm going to try porting [io-uring](https://github.com/ocaml-multicore/ocaml-uring) since it's a simple input data structure (a buffer) but with concurrent semantics for producers and consumers. I've sketched this out as an [MPhil project idea](https://anil.recoil.org/ideas/lean-io-uring-backend) if anyone is keen to pick it up\!

Ilya sets out his vision for auto-formalising programming languages.

### Shriram Krishnamurthi on lightweight diagramming I've been trying to get to [bingo](https://anil.recoil.org/notes/2026w8) on Shriram Krishnamurthi's talks, and he gave _another_ one I hadn't seen before. Today was a delightful ride through the history of [programmatic diagramming](https://diagrams.mingrammer.com/) culminating in a tool called [sPyTial](https://pypi.org/project/spytial-diagramming/) (don't worry, no-one else could figure out how to pronounce it either). The [paper](https://www.siddharthaprasad.com/unpublished/ptkns-spytial.pdf) is to appear at PLDI 2026. > You're working with a tree, a graph, a recursive object -- maybe an AST, a > neural network, or a symbolic term. You don't need an interactive dashboard > or a production-grade visualization system. You just need a diagram, > something that lays it out clearly so you can understand what's going on. > > That's what sPyTial is for. It's designed for developers, educators, and > researchers who work with structured data and need to make that structure > visible — to themselves or to others — with minimal effort. > \-- [sPyTial programming](https://pypi.org/project/spytial-diagramming/) The coolest demonstration was rendering a live binary tree: when dragging a node around, the rendering preserved the tree invariants (left/right children stayed to the left/right, top-down layering stayed top-down), but you could otherwise relocate nodes as you liked in real time. The diagram was a constraint solution, not a fixed layout, and watching the invariants snap back into place was cool. Whenever I do this sort of thing in d3 using force graphs, the result is a mess. sPyTial would fit right into [OCaml notebooks](https://jon.recoil.org/blog/2026/04/odoc_and_ocaml_notebooks.html) especially for visualising the [complex functors](https://anil.recoil.org/papers/2019-mirage-functors) we routinely pile up. It'll take a bit of work because it's built on top of value printers for Python data structures, but I'm thinking that in OCaml we could drive the same pipeline by printing _types_ into values using the same staged meta-programming trick I explored with [Thomas Gazagnaire](https://github.com/samoht) in our old [dyntype](https://anil.recoil.org/papers/2011-dynamics-ml) paper. The technology has come a long way since then though, so I've sketched this out as a [Part II project idea](https://anil.recoil.org/ideas/spytial-ocaml-port).

Shriram Krishnamurthi explains how to pronounce 'spytial'

### Me on TESSERA and planetary computing I had the privilege of closing out the session with a talk on [TESSERA](https://anil.recoil.org/projects/tessera). My argument was that functional programming has a serious role to play in [planetary computing](https://anil.recoil.org/projects/plancomp): we're now generating around half a petabyte of geospatial foundation model embeddings, and I demoed our Zarr v3 cloud-native storage setup, the [geotessera](https://github.com/ucam-eo/geotessera) Python library, the interactive [TZE explorer](https://tze.geotessera.org), and described our experimental [OxCaml inference pipeline](https://www.tunbury.org/2026/02/15/ocaml-tessera/).

Closing out the day with TESSERA talks. Image credit: Aalok Thakkar

An hour before I was due to start, my laptop flat-out refused to connect to the projector. KC offered his laptop, but I had a ton of live demos running locally that I absolutely did not want to lose! Luckily, some frantic Zulip messaging to [Sadiq Jaffer](https://toao.com) got me downloading the right set of files so I could keep the demo services running on my laptop, set up an SSH tunnel to KC's laptop over the IIT-M wifi, and then present from KC's machine while web-browsing to the tunnelled demos on mine. All my messing around with [\##selfhosting](https://anil.recoil.org/tags/selfhosting) does pay off when it comes to emergency jury-rigging in the minutes before a conference talk\! ## Chatting afterwards We had a delightful bunch of conversations outside the formal talks, of course. The undergraduates and PhD students were out in force suggesting ideas to do with OCaml. It was particularly cool to geek out about carbon measurement with [Aalok Thakkar](https://aalok-thakkar.github.io/) from Ashoka University, who travelled down from Delhi to attend. We're going to follow up on [bioacoustics measurements](https://anil.recoil.org/papers/2024-terracorder) and possible uses of TESSERA in his projects.

The happy group after dinner on the eve of the launch!

Payment systems were especially interesting here in India since coming in as a foreigner it's difficult to use [UPI](https://en.wikipedia.org/wiki/Unified_Payments_Interface); [Ryan Gibb](https://ryan.freumh.org) got registered but discovered he couldn't do person-to-person payments with it (only person-to-merchant). I learnt about [Namma Yatri](https://github.com/nammayatri/nammayatri/blob/main/Backend/README.md) which is a public transport system written in Haskell and Purescript which runs a driver-owned cooperative that charges 0% platform fees. This in turn powers things like [Chennai One](https://www.thedailyjagran.com/india/chennai-one-app-launched-how-to-book-tickets-and-travel-across-metro-bus-train-and-auto-with-chennai-ondru-details-10268781) which routes people onto appropriate transport (metro, buses, taxis) to get to their destination. It's pretty cool to see FP being used for homebrew infrastructure in one of the busiest cities in the world\! I also learnt about [Amit Varma's podcast](https://seenunseen.in/) on Indian development and put [Karthik Muralidharan](https://econweb.ucsd.edu/~kamurali/)'s book on "[Accelerating India's Development](https://www.acceleratingindiasdevelopment.in/home)" on my reading list as it seems to make the same arguments as in [Five Times Faster](https://fivetimesfaster.org/) (a book that I loved, but that doesn't seem to have had the impact I'd expected it to). The FP Launchpad feels like a big deal to Indian CS: a well-funded, ambitious, long-horizon centre in a part of the world where there are huge numbers of software engineers but not yet a matching depth of PL research infra. The connections with Cambridge and JS already run deep via [KC Sivaramakrishnan](https://kcsrk.info) and the OxCaml work, but I left with a list of fresh collaborations I want to start too, like [Lean mechanisations](https://anil.recoil.org/ideas/lean-io-uring-backend), causal-synthesis experiments, and a [diagramming port of sPyTial for OCaml](https://anil.recoil.org/ideas/spytial-ocaml-port)\! ### But was the food any good? Why yes, the food was good thank you for asking! Great samosas in IIT Madras, an amazing tasting menu at [Avartana](https://www.itchotels.com/in/en/dining/avartana), and my highlight was [Sashwatha Cafe](https://www.thehindu.com/food/dining/chennais-new-sashwatha-cafe-is-a-posh-karnataka-style-darshini-serving-masala-dosas-and-thatte-idli/article68278865.ece) which had Karnataka darshini that was utterly delicious\!

Sunset over Chennai to close out a very long but very rewarding day

(Videos will become available soon, and I'll update the post with them then) Synopsis: A day at the launch of the FP Launchpad at IIT Madras, covering talks on hardware design, trusted execution on Shakti, verifiable Indian tax law, precise JIT analysis, AI-assisted Lean metatheory, constraint-based diagramming, and my own TESSERA talk. Words: 3228 DOI: 10.59350/4bsr3-h6735 Discussion: - Bluesky: - LinkedIn: - Mastodon: - Twitter: ## Related - [.plan-26-16: Chennai, Cambridge, Belfast: a week on the wing](https://anil.recoil.org/notes/2026w16) (note, 2026-04-19) - [The Bose-Einstein guest house at IIT-Madras](https://anil.recoil.org/videos/85f77768-3a0d-4846-9de0-9424aa3b3678) (video, 2026-04-14) - [.plan-26-15: Banyan trees, (anti)botnets and Bose-Einstein bases](https://anil.recoil.org/notes/2026w15) (note, 2026-04-12) - [The Internet needs an antibotty immune system, stat](https://anil.recoil.org/notes/internet-immune-system) (note, 2026-04-08) - [An io_uring IO implementation for Lean](https://anil.recoil.org/ideas/lean-io-uring-backend) (idea, 2026-04-01) - [A programmatic diagramming library for OCaml](https://anil.recoil.org/ideas/spytial-ocaml-port) (idea, 2026-04-01) - [.plan-26-08: At AI summit, Shriram's PL opinions, Zarr hacking](https://anil.recoil.org/notes/2026w8) (note, 2026-02-22) - [At the AI Impact Summit in Delhi: people, planet, progress](https://anil.recoil.org/notes/india-ai-summit) (note, 2026-02-21) - [Package Managers à la Carte: A Formal Model of Dependency Resolution](https://anil.recoil.org/papers/2026-package-calculus) (paper, 2026-01-01) - [2025 Advent of Agentic Humps: Building a useful O(x)Caml library every day](https://anil.recoil.org/notes/aoah-2025) (note, 2025-12-26) - [Holding an OxCaml tutorial at ICFP/SPLASH 2025](https://anil.recoil.org/notes/icfp25-oxcaml) (note, 2025-10-06) - [Arise Bushel, my sixth generation oxidised website](https://anil.recoil.org/notes/bushel-lives) (note, 2025-01-29) - [OxCaml Labs](https://anil.recoil.org/projects/oxcaml) (project, 2025-01-01) - [TESSERA, a pixelwise geospatial foundation model](https://anil.recoil.org/projects/tessera) (project, 2025-01-01) - [Terracorder: Sense Long and Prosper](https://anil.recoil.org/papers/2024-terracorder) (paper, 2024-08-01) - [Conservation Evidence Copilots](https://anil.recoil.org/projects/ce) (project, 2024-01-01) - [Planetary Computing](https://anil.recoil.org/projects/plancomp) (project, 2022-01-01) - [Information Flow for Trusted Execution](https://anil.recoil.org/projects/difc-tee) (project, 2020-01-01) - [Programming Unikernels in the Large via Functor Driven Development](https://anil.recoil.org/papers/2019-mirage-functors) (paper, 2019-05-01) - [OCaml Labs](https://anil.recoil.org/projects/ocamllabs) (project, 2012-01-01) - [Dynamics for ML using Meta-Programming](https://anil.recoil.org/papers/2011-dynamics-ml) (paper, 2011-07-01) --- Canonical: https://anil.recoil.org/notes/fpl-launch Type: note Tags: ocaml, fp, india, oxcaml, education, tessera