Yong Kiam Tan


I am a second 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 majority of my publications have some form of "verify" in the title.


Scott Owens, Michael Norrish, Ramana Kumar, Magnus O. Myreen, Yong Kiam Tan. Verifying efficient function calls in CakeML. ICFP'17. (preprint,doi)

Anthony Fox, Magnus O. Myreen, Yong Kiam Tan, Ramana Kumar. Verified compilation of CakeML to multiple machine-code targets. CPP'17. (preprint,doi)

Yong Kiam Tan, Magnus O. Myreen, Ramana Kumar, Anthony Fox, Scott Owens, Michael Norrish. A new verified compiler backend for CakeML. ICFP'16. (preprint,doi,slides)

Scott Owens, Magnus O. Myreen, Ramana Kumar, Yong Kiam Tan. Functional big-step semantics. ESOP'16. (preprint,doi)

Yong Kiam Tan, Scott Owens, Ramana Kumar. A verified type system for CakeML. IFL'15. Peter Landin Prize (preprint,doi)


Yong Kiam Tan, Xinxing Xu, Yong Liu. Improved Recurrent Neural Networks for Session-based Recommendations. DLRS'16. (preprint,doi)

Technical Reports

André Platzer, Yong Kiam Tan. How to Prove "All" Dfferential Equation Properties. CMU-CS-17-117. (link)


Yong Kiam Tan. Verified Register Allocation for CakeML. My undergraduate dissertation supervised by Ramana Kumar and Magnus Myreen. (link)


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 )