Functional Programmer at Standard Chartered
Email: jamkhan at connect.hku.hk
[CV] [Scholar] [arXiv] [GitHub] [LinkedIn]
At Standard Chartered, I work on the Cortex financial library, built on Mu (a strict variant of Haskell). I collaborate part-time with Ranjit Jhala on verified constraint solving for refinement types. Previously, I was a Research Intern at MPI-SP with Gilles Barthe, and an undergraduate researcher with Bruno C. d. S. Oliveira at the HKU Programming Languages Group, working on first-class environments, capabilities, and separate compilation.
Research Interests: Type Theory, Functional Programming, Formal Verification, Theorem Provers, and Quantum Computing.
Publications
-
Preprint
-
Complete Relational Logic for Infinite-Dimensional Quantum Programs with Unbounded Assertions
[arXiv] (authors listed alphabetically) -
Capabilities as First-Class Modules with Separate Compilation
[paper] [talk] [poster]
🏅 Gold Award — Undergraduate Category
Positions
-
Standard Chartered — Quantitative Developer Oct 2025 – Present
-
Independent Research Jan 2026 – PresentSupervised by Ranjit Jhala.
Topic: Refinement Types, Verified Constraint Solving, Meta-Programming. -
Max Planck Institute for Security & Privacy — Research Intern Apr – Sept 2025Supervised by Gilles Barthe.
Topic: Formal Verification of Quantum Programs, Relational Logics, Probabilistic Compilation & Quantum Cost Analysis. -
HKU Programming Languages Group — Undergraduate Researcher Aug 2024 – Apr 2025Supervised by Bruno C. d. S. Oliveira.
Topic: Type Systems, Semantics, Mechanization & First-Class Environments. -
HKU Quantum Information and Computation Lab — Research Intern Jun – Aug 2024Supervised by Ravishankar Ramanathan.
Topic: Device-Independent Quantum Key Distribution, Semi-Definite Programming & Bell Non-Locality. -
ActusRayPartners (Hedge Fund) — Technology Intern Jun – Aug 2023
-
All Round Education Academy — Software Developer (Freelance) Mar – Nov 2023
-
HKU Sleep Lab — Student Research Assistant Apr – Oct 2022
Honors & Awards
- Gold Award, ACM Student Research Competition (Undergraduate Category) at PLDI 2025 2025
- Fully-Funded Tuition Scholarship, University of Hong Kong 2021 – 2025
- Fully-Funded Scholarship, Nixor College 2018 – 2020
- Regional Distinction in Computer Science & Physics (GCE A-levels) 2020
Software
- EnvMLHaskell — Source language with elaboration to a core calculus — a variant of System F with first-class environments.
- λSCERocq — Mechanized proofs of type-soundness, semantics preservation, and separate compilation correctness.
- CQOTL ProverOCaml, Lean 4 — Interactive prover for relational properties of classical-quantum programs with extraction to Lean 4.
- TraqHaskell — Haskell package for source-level quantum cost analysis of classical programs.
Talks
- PLanQC 2026 — Contributed talk Jan 2026
- SRC@PLDI 2025 — Capabilities as First-Class Modules with Separate Compilation Jun 2025
Teaching
-
COMP2396 Object-Oriented Programming in Java — Teaching Assistant Fall 2023, Fall 2024University of Hong Kong
-
ENGG1340 Computer Programming in C++ — Teaching Assistant Spring 2023University of Hong Kong
Service
- Student Volunteer, CAV 2025 Jul 2025