Yong Kiam Tan

About

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

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

Journals

• The Verified CakeML Compiler Backend.

  Yong Kiam Tan, Magnus O. Myreen, Ramana Kumar, Anthony Fox, Scott Owens, Michael Norrish.

  JFP. Extended version of our ICFP'16 paper. (preprint)

Conferences

• Vector Barrier Certificates and Comparison Systems.

  Andrew Sogokon, Khalil Ghorbal, Yong Kiam Tan, André Platzer.

  FM'18. (preprint,doi,slides)

• Differential Equation Axiomatization: The Impressive Power of Differential Ghosts.

  André Platzer, Yong Kiam Tan.

  LICS'18. (preprint (with appendix),arXiv,doi,slides)

• Proof-Producing Synthesis of CakeML with I/O and Local State from Monadic HOL Functions.

  Son Ho, Oskar Abrahamsson, Ramana Kumar, Magnus O. Myreen, Yong Kiam Tan and Michael Norrish.

  IJCAR'18. (preprint,doi,slides)

• VeriPhy: Verified controller executables from verified cyber-physical models.

  Brandon Bohrer, Yong Kiam Tan, Stefan Mitsch, Magnus O. Myreen and André Platzer.

  PLDI'18. (preprint,doi)

• Verifying efficient function calls in CakeML.

  Scott Owens, Michael Norrish, Ramana Kumar, Magnus O. Myreen, Yong Kiam Tan.

  ICFP'17. (preprint,doi)

• Verified compilation of CakeML to multiple machine-code targets.

  Anthony Fox, Magnus O. Myreen, Yong Kiam Tan, Ramana Kumar.

  CPP'17. (preprint,doi)

• A new verified compiler backend for CakeML.

  Yong Kiam Tan, Magnus O. Myreen, Ramana Kumar, Anthony Fox, Scott Owens, Michael Norrish.

  ICFP'16. (preprint,doi,slides)

• Functional big-step semantics.

  Scott Owens, Magnus O. Myreen, Ramana Kumar, Yong Kiam Tan.

  ESOP'16. (preprint,doi)

Workshops

• Improved Recurrent Neural Networks for Session-based Recommendations.

  Yong Kiam Tan, Xinxing Xu, Yong Liu.

  DLRS'16. (preprint,doi)

• A verified type system for CakeML.

  Yong Kiam Tan, Scott Owens, Ramana Kumar.

  IFL'15. Peter Landin Prize. (preprint,doi)

Technical Reports

• How to Prove "All" Dfferential Equation Properties.

  André Platzer, Yong Kiam Tan.

  CMU-CS-17-117. (link, superseded by arXiv version and LICS'18 paper)

Others

• Verified Register Allocation for CakeML.

  My undergraduate dissertation supervised by Ramana Kumar and Magnus Myreen. (link)

Contact

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 )