Yong Kiam Tan

About

I am a fifth year graduate 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 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: the word "verify" (or some form of it) appears 13 times in the titles below.

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

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

(*) 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. (arXiv,doi)

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

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

  2. Switched Systems as Hybrid Programs

    Yong Kiam Tan, André Platzer

    ADHS 2021. (arXiv,to appear)

  3. Deductive Stability Proofs for Ordinary Differential Equations

    Yong Kiam Tan, André Platzer

    TACAS 2021. (arXiv,doi,slides)

  4. cake_lpr: Verified Propagation Redundancy Checking in CakeML

    Yong Kiam Tan, Marijn Heule, Magnus O. Myreen

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

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

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

    Fabian Immler, Yong Kiam Tan (*)

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

  7. An Axiomatic Approach to Liveness for Differential Equations

    Yong Kiam Tan, André Platzer

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

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

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

  10. Vector Barrier Certificates and Comparison Systems

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

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

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

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

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

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

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

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

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

Github: https://github.com/tanyongkiam

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