Yong Kiam Tan

About

I defended my PhD thesis in May 2022. Information on this page may be out of date.

I was a graduate student in the Computer Science Department at Carnegie Mellon University.

I was supported by a National Science Scholarship (PhD) from A*STAR, Singapore.

I an an alumnus of the Logical Systems Lab, where I was 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 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. Please use the DOI links for the official publications.

Please let me know if you find any broken links or errors in the preprints.

(*) indicates alphabetical author order.

Journals

  1. An Axiomatic Approach to Existence and Liveness for Differential Equations

    Yong Kiam Tan, André Platzer

    Formal Aspects of Computing (FAOC). Extended version of our FM'19 paper. (arXiv,doi)

  2. Pegasus: Sound Continuous Invariant Generation

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

    Formal Methods in System Design (FMSD). Extended version of our FM'19 paper. (tool,arXiv,doi)

  3. Proof-Producing Synthesis of CakeML from Monadic HOL Functions

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

    Journal of Automated Reasoning (JAR). Extended version of our IJCAR'18 paper. (link,doi)

  4. Differential Equation Invariance Axiomatization

    André Platzer, Yong Kiam Tan (*)

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

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

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

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

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

  1. Implicit Definitions with Differential Equations for KeYmaera X (System Description)

    James Gallicchio, Yong Kiam Tan, Stefan Mitsch, André Platzer

    IJCAR 2022. (arXiv, to appear)

  2. Verified Compilation and Optimization of Floating-Point Programs in CakeML

    Heiko Becker, Robert Rabe, Eva Darulova, Magnus O. Myreen, Zachary Tatlock, Ramana Kumar, Yong Kiam Tan, and Anthony Fox

    ECOOP 2022. (doi)

  3. Verifying Switched System Stability With Logic

    Yong Kiam Tan, Stefan Mitsch, André Platzer

    HSCC 2022. Best Paper Award and Best Repeatability Evaluation Award. (arXiv,doi,slides)

  4. A Verified Decision Procedure for Univariate Real Arithmetic with the BKR Algorithm

    Katherine Cordwell, Yong Kiam Tan, André Platzer

    ITP 2021. (AFP entry,arXiv,doi)

  5. Switched Systems as Hybrid Programs

    Yong Kiam Tan, André Platzer

    ADHS 2021. (arXiv,doi,slides)

  6. Deductive Stability Proofs for Ordinary Differential Equations

    Yong Kiam Tan, André Platzer

    TACAS 2021. (preprint,arXiv,doi,slides)

  7. cake_lpr: Verified Propagation Redundancy Checking in CakeML

    Yong Kiam Tan, Marijn Heule, Magnus O. Myreen

    TACAS 2021. (tool,preprint,doi,slides)

  8. Do You Have Space for Dessert? A Verified Space Cost Semantics for CakeML Programs

    Alejandro Gómez-Londoño, Johannes Åman Pohjola, Hira Taqdees Syeda, Magnus O. Myreen, Yong Kiam Tan

    PACMPL OOPSLA 2020. (preprint,doi)

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

    Fabian Immler, Yong Kiam Tan (*)

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

  10. An Axiomatic Approach to Liveness for Differential Equations

    Yong Kiam Tan, André Platzer

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

  11. 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. (tool,preprint,doi,slides)

  12. 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)

  13. Vector Barrier Certificates and Comparison Systems

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

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

  14. 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)

  15. 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)

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

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

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

  17. Verifying Efficient Function Calls in CakeML

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

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

  18. 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)

  19. 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)

  20. Functional Big-Step Semantics

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

    European Symposium on Programming (ESOP'16). (preprint,doi)

Workshops

  1. Improved Recurrent Neural Networks for Session-based Recommendations

    Yong Kiam Tan, Xinxing Xu, Yong Liu

    DLRS'16. (preprint,doi)

  2. A Verified Type System for CakeML

    Yong Kiam Tan, Scott Owens, Ramana Kumar

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

Technical Reports / Drafts

Others

Theses

Review

I have sub-reviewed for the following conferences and journals: I was also on the PLDI 2020 Artifact Evaluation Committee.

Contact

Office: GHC 6219, Carnegie Mellon University, Pittsburgh, PA 15213

Email: yongkiat (AT) cs.cmu.edu (I may lose direct access to this account, if I do not respond, please try an alternative means of contacting me.)

Email: tanyongkiam (AT) gmail.com (Personal)

Github: https://github.com/tanyongkiam

ORCiD: https://orcid.org/0000-0001-7033-2463

Phone: +1 (412) ( 2 x 2 x 2 x 2 x 3 x 7 x 8269 )