Yong Kiam Tan

About

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.

Research

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.

Publications

Fun fact: 50% (6/12) of my publications have some form of "verify" in the title.

Conferences

Andrew Sogokon, Khalil Ghorbal, Yong Kiam Tan, André Platzer. Vector Barrier Certificates and Comparison Systems. FM'18. (preprint,doi,slides)

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)

Workshops

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

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

Technical Reports

André Platzer, Yong Kiam Tan. How to Prove "All" Dfferential Equation Properties. CMU-CS-17-117. (link, superseded by arXiv version and LICS'18 paper)

Others

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

Contact

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 )