This week I hopped over to Chennai for the launch of the FP Launchpad, 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, who was a postdoc in my OCaml Labs group in Cambridge before moving to IIT Madras as a professor. I eagerly flew in for a couple of days accompanied by Ryan Gibb 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", good timing given the firehose of AI-generated code we are all drinking 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: 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 if you know anyone who would be a good fit!
1 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 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 on the campus where they explain how the IIT was set up with the assistance of the German government.
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 available to get us going.
2 Opening talks
The centre head, KC Sivaramakrishnan, 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, 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.
In a nod to how seriously IIT-M is taking the FPL, the institute's director 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, the RISC-V processor line that has made it into space (which Thomas Gazagnaire will like) 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.
This is a pretty unique situation as far as I'm aware in PL research. In my own use, 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 of the idea being written down.
3 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.
3.1 Rishiyur Nikhil on Bluespec
Rishiyur Nikhil kicked off with a grand unified pitch that "hardware is software, and software is hardware". Bluespec 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.
He walked through property-based testing via QuickCheck in Bluespec, and then presented a test rig that repackages QuickCheck to compare implementations against the official RISC-V formal spec written in 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 years ago in 2015 about how difficult the control logic synthesis process is to automate across arbitrary circuit descriptions.
3.2 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 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, 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 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
- FIDES: End-to-end Compartments for Mixed-language Systems
3.3 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, 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 (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 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, and I imagine they'll connect with Sarvam (the India-specialised LLM trainers I met at the AI Impact Summit earlier this year).
3.4 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 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 does at all at the moment I think.
3.5 Ilya Sergey on an experiment in AI-Assisted Metatheory
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 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 on agentic proof-oriented programming in F*/Pulse (covered in this week's weekly), this is starting to look like an inflection point for mechanised semantics just like in mathematics.
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 has already been using it over the past month to mechanise our 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 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 if anyone is keen to pick it up!
3.6 Shriram Krishnamurthi on lightweight diagramming
I've been trying to get to bingo 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 culminating in a tool called sPyTial (don't worry, no-one else could figure out how to pronounce it either). The paper 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
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 especially for visualising the complex 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 in our old dyntype paper. The technology has come a long way since then though, so I've sketched this out as a Part II project idea.
3.7 Me on TESSERA and planetary computing
I had the privilege of closing out the session with a talk on TESSERA. My argument was that functional programming has a serious role to play in planetary computing: 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 Python library, the interactive TZE explorer, and described our experimental OxCaml inference pipeline.
4 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 from Ashoka University, who travelled down from Delhi to attend. We're going to follow up on bioacoustics measurements and possible uses of TESSERA in his projects.
Payment systems were especially interesting here in India since coming in as a foreigner it's difficult to use UPI; Ryan Gibb got registered but discovered he couldn't do person-to-person payments with it (only person-to-merchant). I learnt about Namma Yatri 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 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 on Indian development and put Karthik Muralidharan's book on "Accelerating India's Development" on my reading list as it seems to make the same arguments as in Five Times Faster (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 and the OxCaml work, but I left with a list of fresh collaborations I want to start too, like Lean mechanisations, causal-synthesis experiments, and a diagramming port of sPyTial for OCaml!
4.1 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, and my highlight was Sashwatha Cafe which had Karnataka darshini that was utterly delicious!
(Videos will become available soon, and I'll update the post with them then)