| 2026 | LICS | Contextual MetaML: Syntax and Full Abstraction. | Haoxuan Yin, Andrzej S. Murawski, C.-H. Luke Ong |
| 2024 | CAV | Unifying Qualitative and Quantitative Safety Verification of DNN-Controlled Systems. | Dapeng Zhi, Peixin Wang, Si Liu, C.-H. Luke Ong, Min Zhang |
| 2023 | ESOP | Fast and Correct Gradient-Based Optimisation for Probabilistic Programming via Smoothing. | Basim Khajwal, C.-H. Luke Ong, Dominik Wagner |
| 2022 | PLDI | Guaranteed bounds for posterior inference in universal probabilistic programming. | Raven Beutner, C.-H. Luke Ong, Fabian Zaiser |
| 2022 | PLDI | CycleQ: an efficient basis for cyclic equational reasoning. | Eddie Jones, C.-H. Luke Ong, Steven J. Ramsay |
| 2021 | ESOP | Densities of Almost Surely Terminating Probabilistic Programs are Differentiable Almost Everywhere. | Carol Mak, C.-H. Luke Ong, Hugo Paquet, Dominik Wagner |
| 2021 | LICS | Supermartingales, Ranking Functions and Probabilistic Lambda Calculus. | Andrew Kenyon-Roberts, C.-H. Luke Ong |
| 2020 | FSCD | The Difference λ-Calculus: A Language for Difference Categories. | Mario Alvarez-Picallo, C.-H. Luke Ong |
| 2019 | ESOP | Fixing Incremental Computation - Derivatives of Fixpoints, and the Recursive Semantics of Datalog. | Mario Alvarez-Picallo, Alex Eyers-Taylor, Michael Peyton Jones, C.-H. Luke Ong |
| 2019 | FOSSACS | Change Actions: Models of Generalised Differentiation. | Mario Alvarez-Picallo, C.-H. Luke Ong |
| 2019 | JELIA | Typed Meta-interpretive Learning of Logic Programs. | Rolf Morel, Andrew Cropper, C.-H. Luke Ong |
| 2019 | LICS | HoCHC: A Refutationally Complete and Semantically Invariant System of Higher-order Logic Modulo Theories. | C.-H. Luke Ong, Dominik Wagner |
| 2018 | LICS | Species, Profunctors and Taylor Expansion Weighted by SMCC: A Unified Framework for Modelling Nondeterministic, Probabilistic and Quantum Programs. | Takeshi Tsukada, Kazuyuki Asada, C.-H. Luke Ong |
| 2018 | TACAS | InterpChecker: Reducing State Space via Interpolations - (Competition Contribution). | Zhao Duan, Cong Tian, Zhenhua Duan, C.-H. Luke Ong |
| 2017 | ESOP | ML and Extended Branching VASS. | Conrad Cotton-Barratt, Andrzej S. Murawski, C.-H. Luke Ong |
| 2017 | LICS | Quantitative semantics of the lambda calculus: Some generalisations of the relational model. | C.-H. Luke Ong |
| 2017 | LICS | Generalised species of rigid resource terms. | Takeshi Tsukada, Kazuyuki Asada, C.-H. Luke Ong |
| 2016 | ESOP | On Hierarchical Communication Topologies in the \pi -calculus. | Emanuele D'Osualdo, C.-H. Luke Ong |
| 2016 | LICS | Plays as Resource Terms via Non-idempotent Intersection Types. | Takeshi Tsukada, C.-H. Luke Ong |
| 2016 | POPL | Unboundedness and downward closures of higher-order pushdown automata. | Matthew Hague, Jonathan Kochems, C.-H. Luke Ong |
| 2015 | FOSSACS | Fragments of ML Decidable by Nested Data Class Memory Automata. | Conrad Cotton-Barratt, David Hopkins, Andrzej S. Murawski, C.-H. Luke Ong |
| 2015 | LATA | Weak and Nested Class Memory Automata. | Conrad Cotton-Barratt, Andrzej S. Murawski, C.-H. Luke Ong |
| 2015 | LICS | Nondeterminism in Game Semantics via Sheaves. | Takeshi Tsukada, C.-H. Luke Ong |
| 2015 | OOPSLA | Detecting redundant CSS rules in HTML5 applications: a tree rewriting approach. | Matthew Hague, Anthony Widjaja Lin, C.-H. Luke Ong |
| 2014 | CSL | Compositional higher-order model checking via | Takeshi Tsukada, C.-H. Luke Ong |
| 2014 | POPL | A type-directed abstraction refinement approach to higher-order model checking. | Steven J. Ramsay, Robin P. Neatherway, C.-H. Luke Ong |
| 2013 | CONCUR | Safety Verification of Asynchronous Pushdown Systems with Shaped Stacks. | Jonathan Kochems, C.-H. Luke Ong |
| 2013 | SAS | Automatic Verification of Erlang-Style Concurrency. | Emanuele D'Osualdo, Jonathan Kochems, C.-H. Luke Ong |
| 2012 | CAV | Hector: An Equivalence Checker for a Higher-Order Fragment of ML. | David Hopkins, Andrzej S. Murawski, C.-H. Luke Ong |
| 2012 | ICALP | Two-Level Game Semantics, Intersection Types, and Recursion Schemes. | C.-H. Luke Ong, Takeshi Tsukada |
| 2012 | ICFP | A traversal-based algorithm for higher-order model checking. | Robin P. Neatherway, Steven J. Ramsay, C.-H. Luke Ong |
| 2011 | ICALP | A Fragment of ML Decidable by Visibly Pushdown Automata. | David Hopkins, Andrzej S. Murawski, C.-H. Luke Ong |
| 2011 | POPL | Verifying higher-order functional programs with pattern-matching algebraic data types. | C.-H. Luke Ong, Steven J. Ramsay |
| 2010 | LICS | Recursion Schemes and Logical Reflection. | Christopher H. Broadbent, Arnaud Carayol, C.-H. Luke Ong, Olivier Serre |
| 2010 | TACAS | Boom: Taking Boolean Program Model Checking One Step Further. | Grard Basler, Matthew Hague, Daniel Kroening, C.-H. Luke Ong, Thomas Wahl, Haoxian Zhao |
| 2009 | CAV | Homer: A Higher-Order Observational Equivalence Model checkER. | David Hopkins, C.-H. Luke Ong |
| 2009 | CONCUR | Winning Regions of Pushdown Parity Games: A Saturation Method. | Matthew Hague, C.-H. Luke Ong |
| 2009 | FOSSACS | On Global Model Checking Trees Generated by Higher-Order Recursion Schemes. | Christopher H. Broadbent, C.-H. Luke Ong |
| 2009 | ICALP | Complexity of Model Checking Recursion Schemes for Fragments of the Modal Mu-Calculus. | Naoki Kobayashi, C.-H. Luke Ong |
| 2009 | LICS | A Type System Equivalent to the Modal Mu-Calculus Model Checking of Higher-Order Recursion Schemes. | Naoki Kobayashi, C.-H. Luke Ong |
| 2009 | LICS | Functional Reachability. | C.-H. Luke Ong, Nikos Tzevelekos |
| 2008 | ESOP | Verification of Higher-Order Computation: A Game-Semantic Approach. | C.-H. Luke Ong |
| 2008 | LICS | Winning Regions of Higher-Order Pushdown Games. | Arnaud Carayol, Matthew Hague, Antoine Meyer, C.-H. Luke Ong, Olivier Serre |
| 2008 | LICS | Collapsible Pushdown Automata and Recursion Schemes. | Matthew Hague, Andrzej S. Murawski, C.-H. Luke Ong, Olivier Serre |
| 2007 | FOSSACS | Symbolic Backwards-Reachability Analysis for Higher-Order Pushdown Systems. | Matthew Hague, C.-H. Luke Ong |
| 2007 | MFCS | Hierarchies of Infinite Structures Generated by Pushdown Automata and Recursion Schemes. | C.-H. Luke Ong |
| 2006 | CSL | Some Results on a Game-Semantic Approach to Verifying Finitely-Presentable Infinite Structures (Extended Abstract). | C.-H. Luke Ong |
| 2006 | LICS | On Model-Checking Trees Generated by Higher-Order Recursion Schemes. | C.-H. Luke Ong |
| 2005 | FOSSACS | Safety Is not a Restriction at Level 2 for String Languages. | Klaus Aehlig, Jolie G. de Miranda, C.-H. Luke Ong |
| 2005 | ICALP | Idealized Algol with Ground Recursion, and DPDA Equivalence. | Andrzej S. Murawski, C.-H. Luke Ong, Igor Walukiewicz |
| 2004 | ICALP | Syntactic Control of Concurrency. | Dan R. Ghica, Andrzej S. Murawski, C.-H. Luke Ong |
| 2004 | LICS | Nominal Games and Full Abstraction for the Nu-Calculus. | Samson Abramsky, Dan R. Ghica, Andrzej S. Murawski, C.-H. Luke Ong, Ian David Bede Stark |
| 2004 | TACAS | Applying Game Semantics to Compositional Software Modeling and Verification. | Samson Abramsky, Dan R. Ghica, Andrzej S. Murawski, C.-H. Luke Ong |
| 2002 | ICALP | Games Characterizing Levy-Longo Trees. | C.-H. Luke Ong, Pietro Di Gianantonio |
| 2002 | LICS | Observational Equivalence of 3rd-Order Idealized Algol is Decidable. | C.-H. Luke Ong |
| 2000 | APLAS | Light Logic and Resource Bounded Computation. | C.-H. Luke Ong |
| 2000 | CSL | Discreet Games, Light Affine Logic and PTIME Computation. | Andrzej S. Murawski, C.-H. Luke Ong |
| 2000 | LICS | Dominator Trees and Fast Verification of Proof Nets. | Andrzej S. Murawski, C.-H. Luke Ong |
| 1999 | CSL | A Universal Innocent Game Model for the Bhm Tree Lambda Theory. | Andrew D. Ker, Hanno Nickau, C.-H. Luke Ong |
| 1997 | POPL | A Curry-Howard Foundation for Functional Computation with Control. | C.-H. Luke Ong, Charles A. Stewart |
| 1996 | LICS | A Semantic View of Classical Proofs: Type-Theoretic, Categorical, and Denotational Characterizations (Preliminary Extended Abstract). | C.-H. Luke Ong |
| 1993 | CSL | A Generic Strong Normalization Argument: Application to the Calculus of Constructions. | C.-H. Luke Ong, Eike Ritter |
| 1993 | LICS | Non-Determinism in a Functional Setting | C.-H. Luke Ong |
| 1992 | ICALP | Lazy Lambda Calculus: Theories, Models and Local Structure Characterization (Extended Abstract). | C.-H. Luke Ong |
| 1988 | FOCS | Fully Abstract Models of the Lazy Lambda Calculus | C.-H. Luke Ong |