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.
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.
André Platzer, Yong Kiam Tan. Differential Equation Axiomatization: The Impressive Power of Differential Ghosts. LICS'18. (preprint (with appendix),arXiv,doi)
Son Ho, Oskar Abrahamsson, Ramana Kumar, Magnus O. Myreen, Yong Kiam Tan and Michael Norrish. Proof-Producing Synthesis of CakeML with I/O and Local State from Monadic HOL Functions. IJCAR'18. (preprint,doi,slides)
Brandon Bohrer, Yong Kiam Tan, Stefan Mitsch, Magnus O. Myreen and André Platzer. VeriPhy: Verified controller executables from verified cyber-physical models. PLDI'18. (preprint,doi)
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)
Email: yongkiat (AT) cs.cmu.edu
Phone: +1 (412) ( 2 x 2 x 2 x 2 x 3 x 7 x 8269 )