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 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

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

(*) indicates alphabetical author order.

Journals

• Differential Equation Invariance Axiomatization.

  André Platzer, Yong Kiam Tan. (*)

  Journal of the ACM (JACM). Extended version of our LICS'18 paper. (arXiv,doi)

• A Formal Safety Net for Waypoint-Following in Ground Robots.

  Brandon Bohrer, Yong Kiam Tan, Stefan Mitsch, Andrew Sogokon, André Platzer.

  IEEE Robotics and Automation Letters (RA-L). (arXiv,doi)

• The Verified CakeML Compiler Backend.

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

  Journal of Functional Programming (JFP). Extended version of our ICFP'16 paper. (preprint,doi)

Conferences

• The Poincaré-Bendixson Theorem in Isabelle/HOL.

  Fabian Immler, Yong Kiam Tan. (*)

  Certified Programs and Proofs (CPP'20). (preprint,doi,slides)

• An Axiomatic Approach to Liveness for Differential Equations.

  Yong Kiam Tan, André Platzer.

  Formal Methods (FM'19). (preprint,arXiv,doi,slides)

• Pegasus: A Framework for Sound Continuous Invariant Generation.

  Andrew Sogokon, Stefan Mitsch, Yong Kiam Tan, Katherine Cordwell, André Platzer.

  Formal Methods (FM'19). Best Tool Paper Award. (preprint,doi,slides)

• Verified Compilation on a Verified Processor.

  Andreas Lööw, Ramana Kumar, Yong Kiam Tan, Magnus O. Myreen, Michael Norrish, Oskar Abrahamsson, Anthony Fox.

  Programming Language Design and Implementation (PLDI'19). (preprint,doi)

• Vector Barrier Certificates and Comparison Systems.

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

  Formal Methods (FM'18). (preprint,doi,slides)

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

  André Platzer, Yong Kiam Tan. (*)

  Logic in Computer Science (LICS'18). (preprint (with appendix),arXiv,doi,slides, minor appendix corrections: 10 Jun 2019)

• 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, Michael Norrish.

  International Joint Conference on Automated Reasoning (IJCAR'18). (preprint,doi,slides)

• VeriPhy: Verified Controller Executables from Verified Cyber-Physical System Models.

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

  Programming Language Design and Implementation (PLDI'18). (preprint,doi)

• Verifying Efficient Function Calls in CakeML.

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

  International Conference on Functional Programming (ICFP'17). (preprint,doi)

• Verified Compilation of CakeML to Multiple Machine-Code Targets.

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

  Certified Programs and Proofs (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.

  International Conference on Functional Programming (ICFP'16). (preprint,doi,slides)

• Functional Big-Step Semantics.

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

  European Symposium on Programming (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 / Drafts

• 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

• ARCH-COMP19 Category Report: Hybrid Systems Theorem Proving.

  Stefan Mitsch, Andrew Sogokon, Yong Kiam Tan, Xiangyu Jin, Bohua Zhan, Shuling Wang, Naijun Zhan. (doi)

• ARCH-COMP18 Category Report: Hybrid Systems Theorem Proving.

  Stefan Mitsch, Andrew Sogokon, Yong Kiam Tan, André Platzer, Hengjun Zhao, Xiangyu Jin, Shuling Wang, Naijun Zhan. (doi)

• Verified Register Allocation for CakeML.

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

Review

• CPP 2019
• ESOP 2020
• ICCPS 2020
• ITP 2016, 2017
• LICS 2019, 2020
• MEMOCODE 2017

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 )