Who am I?
Hi, I'm Kiran (she/her)! I am a Postdoctoral Researcher at the University of Illinois Urbana Champaign, advised by Talia Ringer. Previously I completed my PhD from the National University of Singapore advised by Ilya Sergey in VERSE Lab.
My research focuses on the problem of proof maintenance: developing newer and better tools for the maintenance and automation of formal verification—the process of using computers to construct mathematical proofs about the software correctness—and covers a broad range of techniques, such as proof repair, invariant inference or automated verification.
Notable highlights of my work include: producing the first formally verified proof of the probabilistic properties of the Bloom Filter; inventing proof-driven testing, a novel technique that exploits fundamental mathematical truths (the Curry-Howard correspondence) and enables repairing the proofs of real-world programs.
Other fun facts about me: I am a trans woman (egg cracked 12/2023, started HRT 20/04/2024); I sometimes make games in my free time (my itch.io page), I'm a hobbyist artist and use artwork to capture aspects of my lived experiences, and sometimes I write code.
A selfie of me~
Curriculum Vitae
The latest copy of my CV can be found here.
Contact Me
Feel free to send me an email at mail@kirancodes.me.
I also post under @kirancodes.me on Bluesky! (hey, that's the same domain as this site~)
Publications
Conference Papers
- Concurrent Data Structures Made Easy - OOPSLA 2024 [pdf, code, code(rust)]
Callista Le, Kiran Gopinathan, Koon Wen Lee, Ilya Sergey - Adventure of a Lifetime: Extract Method Refactoring for Rust - OOPSLA 2023 [pdf, code]
Sewen Thy, Andrea Costea, Kiran Gopinathan, Ilya Sergey - Rhombus: A New Spin on Macros Without All the Parentheses - OOPSLA 2023 [pdf, code]
Matthew Flatt, Taylor Allred, Nia Angle, Stephen De Gabrielle, Robert Bruce Findler, Jack Firth, Kiran Gopinathan, Ben Greenman, Siddhartha Kasivajhula, Alex Knauth, Jay McCarthy, Sam Phillips, Sorawee Porncharoenwase, Jens Axel Søgaard, Sam Tobin-Hochstadt - Mostly Automated Proof Repair for Verified Libraries - PLDI 2023 [pdf, slides, code]
Kiran Gopinathan, Mayank Keoliya, Ilya Sergey
ACM SIGPLAN Award Awarded ACM SIGPLAN Distinguished Paper Award - Certifying the Synthesis of Heap-Manipulating Programs - ICFP 2021 [pdf, code]
Yasunari Watanabe, Kiran Gopinathan, George Pîrlea, Nadia Polikarpova, Ilya Sergey - Ceramist: Certifying Certainty and Uncertainty in Approximate Membership Query Structures - CAV 2020 [pdf, slides, poster, code]
Kiran Gopinathan, Ilya Sergey - FHIR-FLI: An Open Source Platform for Sharing Healthcare Data - ICT4AWE 2018
Kiran Gopinathan, Nikolaos Alexandros Kaloumenos, Kinnari Ajmera, Alexandru Matei, Ian Williams, Andrew Davis
Workshop Papers
- Towards Optimising Certified Programs by Proof Rewriting - EGRAPHS 2022 [pdf, slides]
Kiran Gopinathan, Ilya Sergey - GopCaml: A Structural Editor for OCaml - OCaml Workshop 2021 [pdf, slides, code]
Kiran Gopinathan - Probchain: Towards Mechanising Probabilistic Properties of a Blockchain - CoqPL 2019 [pdf, slides, code]
Kiran Gopinathan, Ilya Sergey
Awards
- NUS School of Computing Dean's Graduate Research Excellence Award 2023
Given to senior PhD students who have made significant research achievements during their PhD study. - ACM SIGPLAN Distinguished Paper Award, PLDI 2023
Recieved a distinguished paper award for my work on "Mostly Automated Proof Repair for Verified Libraries". - Silver Medal for Student Research Competition, PLDI 2020
For poster and presentation on Certifying Bloom Filters.
Service
Mentoring, Volunteering and Event Organisation
- SIGPLAN-M (Long-term External Mentoring for PhD Students and Researchers), 2022-present
Member of the Operations Team - NUS Programming Languages and Software Engineering (PLSE) Website, 2022-present
Developed and maintained the website for NUS's PLSE groups
Designed the logo for the NUS PLSE social media account - Asian Symposium on Programming Languages and Systems 2022
Designed the badges given for artefact evaluation results - NUS Programming Languages Mentoring Workshop (PLMW) at OOPSLA 2021
Panellist on the PhD Life Panel - NUS Computing Research Week 2021
Organised and ran NUS' internal research week conference as the Program Chair - Symposium on Implementation and Application of Functional Languages 2019
Served as a Student volunteer
Program Committee Member
- ICFP 2025
- OCaml Workshop 2023
- AIPLANS 2021
External Reviewer
- ICSE 2024
- OOPSLA 2023
- POPL 2022
- ESOP 2022
- CPP 2021
- CPP 2020
Artefact Evaluation Committee
- PLDI 2021
- ICFP 2021
- PLDI 2020
Teaching
- CS6217: Topics in Programming Languages & Software Engineering, 2023 - Guest Lecturer
Gave seminar on "Program Logics for Functional Languages" - CS5232: Formal Specification and Design Techniques, 2023 - Guest Lecturer
Gave seminar on Dafny and "Introduction to Floyd-Hoare Logic" - CS5223: Distributed Systems, 2020-2023 - Teaching Assistant
- CS4215: Programming Languages Implementation, 2020-2022 - Teaching Assistant
- CS5218: Principles and Practice of Program Analysis, 2021 - Teaching Assistant
- CS1010E: Programming Methodology, 2019 - Teaching Assistant
Notable Projects & Software
- Sisyphus: Tool for automated repair of proofs of OCaml programs [code]
- Cleango: Clingo bindings and DSL for Lean4 (10 Stars) [code]
- Ceramist: Verified hash-based Bloom Filters in Coq (120 Stars) [code]
- Gopcaml mode: Emacs plugin Structural editing of OCaml code [code]
- Petrol: Typed SQL DSL for OCaml (85 Stars) [code]
- Ego: Pure OCaml E-graphs library (50 Stars) [code]
- OCamlot: Activitypub server in OCaml (64 Stars) [code]