Yong Kiam Tan


I am a third year PhD student in the Computer Science Department at Carnegie Mellon University.

I am supported by a National Science Scholarship (PhD) from A*STAR, Singapore.

I am a member of the Logical Systems Lab, where I am fortunate to be advised by Prof. André Platzer.


I am interested in proof theory for Differential Dynamic Logic (dL).

In particular, I am studying the continuous fragment of dL, which allows users to syntactically reason about (systems of) ordinary differential equations.

I also contribute regularly to the KeYmaera X theorem prover.

I am also a developer of the CakeML compiler, which is formally verified in the HOL4 theorem prover.


Fun fact: the word "verify" (or some form of it) appears 11 times in the titles below.




Technical Reports / Drafts



Office: GHC 7513, Carnegie Mellon University, Pittsburgh, PA 15213

Email: yongkiat (AT) cs.cmu.edu

Github: https://github.com/tanyongkiam

Phone: +1 (412) ( 2 x 2 x 2 x 2 x 3 x 7 x 8269 )

ORCID iD iconhttps://orcid.org/0000-0001-7033-2463