Title: A Mechanically Verified Garbage Collector for OCaml

Speaker: KC Sivaramakrishnan    (bio) (bio)

KC Sivaramakrishnan is an Assistant Professor in the Computer Science and Engineering department at Indian Institute of Technology, Madras and the Chief Technology Officer of Tarides. He led the development of Multicore OCaml, a concurrent and parallel extension of the OCaml programming language. His research interest lies in building robust, secure and scalable systems using programming language technology.

When: Tuesday, 18 November 2025 at 1900 hrs (IST)  

Meeting Details: Zoom link, ID: 891 6409 4870, Passcode: 082194

Abstract:
OCaml is a garbage-collected (GC) language, where unused memory is automatically and reliably freed. OCaml's GC is known for its high throughput and low latency, making it suitable for both batch jobs and interactive systems. OCaml GC is non-trivial and written in C, and is a part of the trusted computing base of OCaml programs. Bugs in the GC have the potential to violate the type safety of OCaml programs. In this talk, I will describe our work in developing a correct, proof-oriented GC for OCaml from scratch, capable of being swapped into the existing OCaml runtime system. Our GC is simple — a stop-the-world mark-and-sweep collector — but is capable of running non-trivial OCaml programs. The GC is developed in F* and its low-level subset Low*, which is compiled to memory-safe C. I will also describe the extension of our collector to enable generational and incremental collection.

This work was published in the Journal of Automated Reasoning (link).