Yong Kiam Tan

About

I am a research scientist in the Cybersecurity department at the Institute for Infocomm Research, A*STAR, Singapore.

I completed my PhD in Computer Science (Pure and Applied Logic) at Carnegie Mellon University, where 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. My PhD thesis was awarded the CMU SCS Distinguished Dissertation Award 2022.

Research

I am interested in applications of deductive verification and interactive theorem proving in automated reasoning, compilers, formalized mathematics, hybrid systems, and security (cryptography).

Please get in touch with me (contacts below) if you are interested in collaborating on these topics.

My PhD thesis examined the proof theory of Differential Dynamic Logic (dL), in particular, the continuous fragment of dL, which allows users to syntactically reason about (systems of) ordinary differential equations.

I contributed to the KeYmaera X theorem prover for hybrid systems. Specifically, I developed much of its differential equation and switched system automation.

I am a developer of the CakeML compiler, which is formally verified in the HOL4 theorem prover.

I am also an amateur user of Isabelle/HOL, here are my AFP entries.

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. Verified propagation redundancy and compositional UNSAT checking in CakeML

    Yong Kiam Tan, Marijn Heule, Magnus O. Myreen

    Software Tools for Technology Transfer (STTT). Extended version of our TACAS'21 paper. To appear

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

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

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

  5. Differential Equation Invariance Axiomatization

    André Platzer, Yong Kiam Tan (*)

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

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

  7. 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 First Complete Algorithm for Real Quantifier Elimination in Isabelle/HOL

    Katherine Cordwell, Yong Kiam Tan, André Platzer

    CPP 2023. To appear

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

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

    IJCAR 2022. (arXiv, doi)

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

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

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

  6. Switched Systems as Hybrid Programs

    Yong Kiam Tan, André Platzer

    ADHS 2021. (arXiv,doi,slides)

  7. Deductive Stability Proofs for Ordinary Differential Equations

    Yong Kiam Tan, André Platzer

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

  8. cake_lpr: Verified Propagation Redundancy Checking in CakeML

    Yong Kiam Tan, Marijn Heule, Magnus O. Myreen

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

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

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

    Fabian Immler, Yong Kiam Tan (*)

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

  11. An Axiomatic Approach to Liveness for Differential Equations

    Yong Kiam Tan, André Platzer

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

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

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

  14. Vector Barrier Certificates and Comparison Systems

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

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

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

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

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

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

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

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

  21. 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: S10C089, Institute for Infocomm Research, 1 Fusionopolis Way, #21-01 Connexis, Singapore 138632

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

Email: tan_yong_kiam (AT) i2r.a-star.edu.sg (Work)

Phone: (+65) 7 * (12345678 + 996193) (Email preferred)

Github: https://github.com/tanyongkiam

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

CV: please contact me through one of the methods above

FAQ

Q: Why does this webpage look like it was made in the 1990s?

A: It was the easiest option for me. If you are unable to (efficiently) find what you are looking for on this page, please let me know.