Yong Kiam Tan


I am a fourth year graduate 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 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 12 times in the titles below.

Preprints are made available below for your personal use. Use the DOI links for the official publication.

(*) indicates alphabetical author order.




Technical Reports / Drafts



I have sub-reviewed for the following conferences:


Office: GHC 6219, 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 )