Functional Programmer at Standard Chartered
Email: jamkhan at connect.hku.hk
[CV] [Scholar] [GitHub] [LinkedIn]
I work in Standard Chartered's Core Strats team on build tooling, runtime support, and compiler extensions for Mu (a strict variant of Haskell). I collaborate with Ranjit Jhala and Nico Lehmann at UC San Diego on proof-producing constraint solving and refinement types, and with Bruno C. d. S. Oliveira at the HKU Programming Languages Group on first-class environments and separate compilation. Previously, I was a research intern at MPI-SP, working with Gilles Barthe and Michael Walter on quantum program verification and cost analysis.
Research Interests: Type systems, program logics, Horn solving, refinement types, and quantum verification.
News
Show earlier news… Show less
Publications
Peer-reviewed papers
-
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
Manuscripts
-
Submitted
-
Submitted
-
Preprint
arXiv -
In preparationLinking as Evaluation: Separate Compilation with First-Class Environments
Software
-
FlexLean4Certified constrained Horn clause (CHC) solving for expressive refinement typing.
-
SMTLib-to-Lean4Lean4Translation of SMT queries, including CHCs, into Lean4 propositions.
-
EnvMLHaskellAn 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
Teaching
-
COMP2396 Object-Oriented Programming in Java Fall 2024, Fall 2023Teaching Assistant, University of Hong Kong
Instructor: Kenneth Wong -
ENGG1340 Computer Programming in C++ Spring 2023Teaching Assistant, University of Hong Kong
Instructor: Dr. Tat Wing Chim (T. W. Chim) -
Mathematics & Computer Science Feb 2022 – Aug 2023Tutor, All Round Education Academy, Hong Kong