I am Kwing Hei “Heili” Li, a PhD Student in the Logics and Semantics group at Aarhus University. My supervisor is Lars Birkedal.

I develop higher-order separation logics to reason about higher-order probabilistic programs, especially those that might involve concurrency. I am also interested in other relatively theoretical aspects of programming languages, especially type theory. Most of my research is formalized in the Coq proof assistant under the Iris logic framework. The only situations when I have to resort to pen-and-paper proofs are the times when I accidentally left my laptop at home; I am intelligent enough to not trust my calculations and God forbid I attempt to read my own handwriting.

Before that, I was an MPhil in Advanced Computer Science student at King’s College, University of Cambridge. And before that, I was a Computer Science with Mathematics undergraduate at Churchill College, University of Cambridge.

My favourite mammal is the donkey.

BACK to home page