Home

I’m Kwing Hei Li, or simply Heili. I can run down stairs really fast.

Click HERE for more info about me.

Preprints

• Modular Verification of Differential Privacy in Probabilistic Higher-Order Separation Logic
  P. G. Haselwarter, A. Aguirre, S. O. Gregersen, K. H. Li, J. Tassarotti, L. Birkedal

• Contextual Refinement of Higher-Order Concurrent Probabilistic Programs (arXiv)
  K. H. Li, A. Aguirre, J. Tassarotti, L. Birkedal

Publications

• Modular Reasoning about Error Bounds for Concurrent Probabilistic Programs (PDF)
  K. H. Li, A. Aguirre, S. O. Gregersen, P. G. Haselwarter, J. Tassarotti, L. Birkedal
  ICFP 2025

• Approximate Relational Reasoning for Higher-Order Probabilistic Programs (PDF)
  P. G. Haselwarter, K. H. Li, A. Aguirre, S. O. Gregersen, J. Tassarotti, L. Birkedal
  POPL 2025

• Tachis: Higher-Order Separation Logic with Credits for Expected Costs (PDF)
  P. G. Haselwarter, K. H. Li, M. de Medeiros, S. O. Gregersen, A. Aguirre, J. Tassarotti, L. Birkedal
  OOPSLA 2024

• Error Credits: Resourceful Reasoning about Error Bounds for Higher-Order Probabilistic Programs (PDF)
  A. Aguirre, P. G. Haselwarter, M. de Medeiros, K. H. Li, S. O. Gregersen, J. Tassarotti, L. Birkedal
  ICFP 2024
  Distinguished Paper Award

• Secure Aggregation for Federated Learning in Flower (PDF)
  K. H. Li, P. P. B. de Gusmão, D. J. Beutel, N. D. Lane
  DistributedML 2021

Unpublished Notes

• Wait-Free Task Solvability of Asynchronous Distributed Models (PDF)
  K. H. Li
  Masters thesis, 2023

• Flower: A Friendly Federated Learning Research Framework (PDF)
  D. J. Beutel, T. Topal, A. Mathur, X. Qiu, J. Fernandez-Marques, Y. Gao, L. Sani, K. H. Li, T. Parcollet, P. P. B. de Gusmão, N. D. Lane
  2022

• Type Systems for Functional Reactive Programming (PDF)
  K. H. Li
  Bachelor thesis, 2022

Talks

• Separation Logics for Probability, Concurrency, and Security (Slides)
  Doctoral Symposium 2025

• Coneris: Modular Reasoning about Error Bounds for Concurrent Probabilistic Programs (Slides)
  Logsem Seminar 2025 + Iris Workshop 2025

• The Asynchronous Computability Theorem - A Marriage Between Distributed Systems and Algebraic Topology (Slides, Recording)
  Churchill CompSci Talks 2022

• Understanding the Source Coding Theorem - A Talk on Shannon’s Entropy (Slides)
  Churchill CompSci Talks 2021
  Audience Favourite Talk Prize

Misc

Photo (2023 May Bumps)

Other stuff