Industry. I work full-time as a functional programmer in Standard Chartered's Core Strats team, developing core infrastructure for Mu, our internal Haskell variant. My work spans the compiler, build systems, gRPC, and protobuf compiler for Haskell.
Research.
I currently conduct research on proof-producing Horn solving in Lean 4
and its application to expressive refinement types, working remotely under
Ranjit Jhala
in the UCSD Progsys Group.
Previously, I was a research intern at the
Max Planck Institute for Security and Privacy (MPI-SP),
conducting research on program logics and cost analysis for quantum programs
under supervision of Gilles Barthe.
I also worked on type systems and language design in the
HKU Programming Languages Group,
under the supervision of
Bruno C. d. S. Oliveira.
I'm broadly interested in programming languages and verification. Research is most fun as a dialogue between theory and practice: turning elegant theories into practical systems, then using those systems at scale to expose the limits of theories and then, find better theories and abstractions. Repeat!
News
Show earlier news… Show less
Research Papers
-
In submission
-
In submission
-
Complete Relational Logic for Infinite-Dimensional Quantum Programs with Unbounded Assertions
Authors listed alphabetically. -
Capabilities as First-Class Modules with Separate Compilation
[Paper] [Talk] [Poster]
Gold Award — Undergraduate Category
-
Manuscript
-
Manuscript
Software
-
FlexLean4Proof-producing constrained Horn clause (CHC) solving for expressive refinement typing.
-
SMTLib-to-Lean4Lean4Translation of SMT queries, including CHCs, into Lean4 propositions.
-
EnvMLHaskell, RocqAn ML-like language with dynamic module composition, elaborated to a variant of System F with first-class environments.
-
SCEOCaml, Lean4A mechanized calculus for first-class linking and separate compilation, with a compiler and WebAssembly backend.
-
cqOTL ProverOCaml, Lean 4Interactive prover for relational properties of classical-quantum programs with extraction to Lean 4.
-
TraqHaskellHaskell package for source-level quantum cost analysis of classical programs.
Talks
- HKU PL Seminar — Flex: Proof-producing CHC solver [slides] Sept 2026
- PLanQC 2026 — Traq: Estimating the Quantum Cost of Classical Programs [slides] [extended abstract] [talk] Jan 2026
- PLDI 2025 SRC — Capabilities as First-Class Modules with Separate Compilation [talk] [poster] Jun 2025
- HKU Seminar — Maximal Violation of a Measurement Protocol with Simplex Bell Inequality [slides] Aug 2024
Honors & Awards
- Gold Award, ACM Student Research Competition (Undergraduate Category) at PLDI 2025 2025
- HKU Undergraduate Entrance Scholarship for Outstanding Academic Talents 2022 – 2024
- HKSAR Government Scholarship Fund 2021 – 2024
- Rosita King Ho Scholarship 2024
- Cathay Hackathon — 2nd Runner-up (won flight to Boston, USA) 2023
- HKU Foundation Entrance Scholarship 2021
- Top in Sindh & Balochistan (GCE A-levels, Computer Science & Physics) 2020
- 100% Merit Scholarship for GCE A-levels, Nixor College 2018 – 2020