Research at FP Launchpad spans programming languages, systems, and formal verification, with a particular focus on the O(x)Caml ecosystem. The work below reflects the research interests of our faculty, and forms the foundation for ongoing and future projects at the centre.

Effect Handlers & Language Design

PLT OCaml

Algebraic effect handlers offer a principled, composable abstraction for programming with side effects, unifying exceptions, async I/O, and coroutines under a single framework. This line of work spans foundational theory, compilation strategies, and practical integration into OCaml and WebAssembly.

Related open source work: OCaml 5: Multicore & Algebraic Effects

  • Continuing WebAssembly with Effect Handlers — Luna Phipps-Costin et al. (OOPSLA 2023)
  • Eio 1.0 – Effects-based IO for OCaml 5 — Thomas Leonard et al. (OCaml Workshop 2023)
  • Composing Schedulers using Effect Handlers — Deepali Ande, KC Sivaramakrishnan (OCaml Workshop 2022)
  • Retrofitting Effect Handlers to OCaml — KC Sivaramakrishnan et al. (PLDI 2021)
  • Experiences with Effects — Thomas Leonard et al. (OCaml Workshop 2021)
  • Concurrent System Programming with Effect Handlers — Stephen Dolan et al. (TFP 2017)
  • Continuation Passing Style for Effect Handlers — Daniel Hillerström et al. (FSCD 2017)
  • Eff Directly in OCaml — Oleg Kiselyov, KC Sivaramakrishnan (ML Workshop 2016)
  • Compiling Links Effect Handlers to the OCaml Backend — Daniel Hillerström et al. (ML Workshop 2016)
  • Effectively Tackling the Awkward Squad — Stephen Dolan et al. (ML Workshop 2017)
  • Effective Concurrency with Algebraic Effects — Stephen Dolan et al. (OCaml Workshop 2015)
  • Effectively Composing Concurrency Libraries — Deepali Ande et al. (Working Draft 2023)

Concurrency & Parallelism

OCaml Systems

Building the theory and infrastructure for safe, scalable concurrent and parallel programming. The flagship contribution is Multicore OCaml, which introduced parallel domains and effect handlers into OCaml 5, alongside work on scheduling, lock-free data structures, and testing tools for concurrent programs.

Related open source work: OCaml 5: Multicore & Algebraic Effects, Multicore Runtimes & Performance

  • Retrofitting Parallelism onto OCaml — KC Sivaramakrishnan et al. (ICFP 2020, Distinguished Paper)
  • Parallelising your OCaml Code with Multicore OCaml — Sadiq Jaffer et al. (OCaml Workshop 2020)
  • Adapting the OCaml Ecosystem for Multicore OCaml — Sudha Parimala et al. (OCaml Workshop 2021)
  • Parafuzz: Coverage-guided Property Fuzzing for Multicore OCaml — Sumit Padhiyar et al. (OCaml Workshop 2021)
  • Building a Lock-free STM for OCaml — Vesa Karvonen et al. (OCaml Workshop 2023)
  • Lock-free Programming for the Masses — KC Sivaramakrishnan, Théo Laurent (OCaml Workshop 2016)
  • ConFuzz: Coverage-guided Property Fuzzing for Event-driven Programs — Sumit Padhiyar, KC Sivaramakrishnan (PADL 2023, Distinguished Paper)
  • Composable Scheduler Activations for Haskell — KC Sivaramakrishnan et al. (JFP 2016)
  • MultiMLton: A Multicore-aware Runtime for Standard ML — KC Sivaramakrishnan et al. (JFP 2014)
  • Rx-CML: A Prescription for Safely Relaxing Synchrony — KC Sivaramakrishnan et al. (PADL 2014)
  • Composable Asynchronous Events — Lukasz Ziarek et al. (PLDI 2011)
  • Migrating MultiMLton to the Cloud — KC Sivaramakrishnan et al. (ML Workshop 2013)
  • Scalable Lightweight Task Management Schemes for MIMD Processors — Daniel Waddington et al. (SFMA 2011)
  • Featherweight Threads for Communication — KC Sivaramakrishnan et al. (Purdue TR 2011)
  • Design Rationale for MultiMLton — Suresh Jagannathan et al. (ML Workshop 2010)
  • Lightweight Asynchrony using Parasitic Threads — KC Sivaramakrishnan et al. (DAMP 2010)
  • Partial Memoization of Concurrency and Communication — Lukasz Ziarek et al. (ICFP 2009)

Distributed Systems & Consistency

Systems

Programming language approaches to the challenges of distributed consistency, including mergeable replicated data types, coordination-free transactions, and declarative models for eventually consistent stores. This work shows how functional abstractions can tame the complexity of weak consistency.

Related open source work: Distributed & Eventually Consistent Systems

  • Sal: Multi-modal Verification of Replicated Data Types — Pranav Ramesh et al. (Working Draft 2026)
  • Automatically Verifying Replication-aware Linearizability — Vimala Soundarapandian et al. (OOPSLA 2025)
  • Certified Mergeable Replicated Datatypes — Vimala Soundarapandian et al. (PLDI 2022)
  • Marrying Replicated and Functional Data Structures — Vimala Soundarapandian et al. (PaPoC 2022)
  • Certified Mergeable Replicated Data Types — Vimala Soundarapandian et al. (PaPoC 2021)
  • Banyan: Coordination-free Distributed Transactions over Mergeable Types — Shashank Dubey et al. (APLAS 2020)
  • Mergeable Replicated Data Types — Gowtham Kaki et al. (OOPSLA 2019)
  • Version Control Is For Your Data Too — Gowtham Kaki et al. (SNAPL 2019)
  • Safe Replication through Bounded Concurrency Verification — Gowtham Kaki et al. (OOPSLA 2018)
  • An Architecture for Interspatial Communication — Anil Madhavapeddy et al. (HotPOST 2018)
  • DaLi: Database as a Library — Gowtham Kaki et al. (SNAPL 2017)
  • Mergeable Types — Gowtham Kaki et al. (ML Workshop 2017)
  • Representation without Taxation — KC Sivaramakrishnan et al. (IEEE Data Engineering Bulletin 2016, Invited)
  • Declarative Programming over Eventually Consistent Data Stores — KC Sivaramakrishnan et al. (PLDI 2015)
  • Functional Programming Abstractions for Weakly Consistent Systems — KC Sivaramakrishnan (PhD Dissertation, Purdue 2014)

Memory Management & Runtime Systems

OCaml Systems

Designing and verifying the runtime substrate of functional languages, from garbage collectors to memory models. This work includes a mechanically verified GC for OCaml and techniques for reducing runtime overheads in concurrent settings.

Related open source work: Multicore Runtimes & Performance

  • A Mechanically Verified Garbage Collector for OCaml — Sheera Shamsu et al. (Journal of Automated Reasoning 2025)
  • A Mechanically Verified Garbage Collector for OCaml — Sheera Shamsu et al. (OCaml Workshop 2025)
  • Bounding Data Races in Space and Time — Stephen Dolan et al. (PLDI 2018)
  • A Memory Model for Multicore OCaml — Stephen Dolan, KC Sivaramakrishnan (OCaml Workshop 2017)
  • A Coherent and Managed Runtime for ML on the SCC — KC Sivaramakrishnan et al. (MARC 2012, Best Paper)
  • Eliminating Read Barriers through Procrastination and Cleanliness — KC Sivaramakrishnan et al. (ISMM 2012)

Formal Verification & Safety

PLT

Applying formal methods to verify correctness and security properties of systems. This includes session types for safe distributed interaction, mechanised proofs for critical infrastructure, and compartmentalisation for mixed-language security.

  • FIDES: End-to-end Compartments for Mixed-language Systems — Sai Venkata Krishnan et al. (AsiaCCS 2026)
  • TallyGuard: Privacy Preserving Tallied-as-cast Guarantee — Athish Pranav Dharmalingam et al. (Working Draft 2025)
  • Efficient Sessions — KC Sivaramakrishnan et al. (Science of Computer Programming 2014)
  • Efficient Session Type Guided Distributed Interaction — KC Sivaramakrishnan et al. (COORDINATION 2010, Distinguished Paper)