Fully Abstract Models of the Lazy Lambda Calculus - C.-H. Luke Ong (FOCS, 1988)

Lazy Lambda Calculus: Theories, Models and Local Structure Characterization (Extended Abstract). - C.-H. Luke Ong (ICALP, 1992)

A Generic Strong Normalization Argument: Application to the Calculus of Constructions. - C.-H. Luke Ong; Eike Ritter (CSL, 1993)

Non-Determinism in a Functional Setting - C.-H. Luke Ong (LICS, 1993)

Modified Realizability Toposes and Strong Normalization Proofs. - J. M. E. Hyland; C.-H. Luke Ong (TLCA, 1993)

Full Abstraction in the Lazy Lambda Calculus - Samson Abramsky; C.-H. Luke Ong (Inf. Comput., 1993)

Pi-Calculus, Dialogue Games and PCF. - J. M. E. Hyland; C.-H. Luke Ong (FPCA, 1995)

A Semantic View of Classical Proofs: Type-Theoretic, Categorical, and Denotational Characterizations (Preliminary Extended Abstract). - C.-H. Luke Ong (LICS, 1996)

A Curry-Howard Foundation for Functional Computation with Control. - C.-H. Luke Ong; Charles A. Stewart (POPL, 1997)

A Universal Innocent Game Model for the Böhm Tree Lambda Theory. - Andrew D. Ker; Hanno Nickau; C.-H. Luke Ong (CSL, 1999)

Internal Languages for Autonomous and *-Autonomous Categories. - Thong wei Koh; C.-H. Luke Ong (CTCS, 1999)

Exhausting Strategies, Joker Games and IMLL with Units. - Andrzej S. Murawski; C.-H. Luke Ong (CTCS, 1999)

Light Logic and Resource Bounded Computation. - C.-H. Luke Ong (APLAS, 2000)

Discreet Games, Light Affine Logic and PTIME Computation. - Andrzej S. Murawski; C.-H. Luke Ong (CSL, 2000)

Dominator Trees and Fast Verification of Proof Nets. - Andrzej S. Murawski; C.-H. Luke Ong (LICS, 2000)

On Full Abstraction for PCF: I, II, and III. - J. M. E. Hyland; C.-H. Luke Ong (Inf. Comput., 2000)

Evolving Games and Essential Nets for Affine Polymorphism. - Andrzej S. Murawski; C.-H. Luke Ong (TLCA, 2001)

Model Checking Algol-Like Languages Using Game Semantics. - C.-H. Luke Ong (FSTTCS, 2002)

Observational Equivalence of 3rd-Order Idealized Algol is Decidable. - C.-H. Luke Ong (LICS, 2002)

Route oscillations in I-BGP with route reflection. - Anindya Basu; Chih-Hao Luke Ong; April Rasala; F. Bruce Shepherd; Gordon T. Wilfong (SIGCOMM, 2002)

Innocent game models of untyped lambda-calculus. - Andrew D. Ker; Hanno Nickau; C.-H. Luke Ong (Theor. Comput. Sci., 2002)

Adapting innocent game models for the Böhm treelambda -theory. - Andrew D. Ker; Hanno Nickau; C.-H. Luke Ong (Theor. Comput. Sci., 2003)

Exhausting strategies, joker games and full completeness for IMLL with Unit. - Andrzej S. Murawski; C.-H. Luke Ong (Theor. Comput. Sci., 2003)

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 (LICS, 2004)

Applying Game Semantics to Compositional Software Modeling and Verification. - Samson Abramsky; Dan R. Ghica; Andrzej S. Murawski; C.-H. Luke Ong (TACAS, 2004)

An approach to deciding the observational equivalence of Algol-like languages. - C.-H. Luke Ong (Ann. Pure Appl. Log., 2004)

On an interpretation of safe recursion in light affine logic. - Andrzej S. Murawski; C.-H. Luke Ong (Theor. Comput. Sci., 2004)

Games characterizing Levy-Longo trees. - C.-H. Luke Ong; Pietro Di Gianantonio (Theor. Comput. Sci., 2004)

Safety Is not a Restriction at Level 2 for String Languages. - Klaus Aehlig; Jolie G. de Miranda; C.-H. Luke Ong (FoSSaCS, 2005)

Idealized Algol with Ground Recursion, and DPDA Equivalence. - Andrzej S. Murawski; C.-H. Luke Ong; Igor Walukiewicz (ICALP, 2005)

The Monadic Second Order Theory of Trees Given by Arbitrary Level-Two Recursion Schemes Is Decidable. - Klaus Aehlig; Jolie G. de Miranda; C.-H. Luke Ong (TLCA, 2005)

Some Results on a Game-Semantic Approach to Verifying Finitely-Presentable Infinite Structures (Extended Abstract). - C.-H. Luke Ong (CSL, 2006)

On Model-Checking Trees Generated by Higher-Order Recursion Schemes. - C.-H. Luke Ong (LICS, 2006)

Syntactic control of concurrency. - Dan R. Ghica; Andrzej S. Murawski; C.-H. Luke Ong (Theor. Comput. Sci., 2006)

Fast verification of MLL proof nets via IMLL. - Andrzej S. Murawski; C.-H. Luke Ong (ACM Trans. Comput. Log., 2006)

Fully abstract semantics of additive aspects by translation. - Sam Bakhtiar Sanjabi; C.-H. Luke Ong (AOSD, 2007)

Hierarchies of Infinite Structures Generated by Pushdown Automata and Recursion Schemes. - C.-H. Luke Ong (MFCS, 2007)

Verification of Higher-Order Computation: A Game-Semantic Approach. - C.-H. Luke Ong (ESOP, 2008)

Winning Regions of Higher-Order Pushdown Games. - Arnaud Carayol; Matthew Hague; Antoine Meyer; C.-H. Luke Ong; Olivier Serre (LICS, 2008)

Symbolic Backwards-Reachability Analysis for Higher-Order Pushdown Systems. - Matthew Hague; C.-H. Luke Ong (Log. Methods Comput. Sci., 2008)

Homer: A Higher-Order Observational Equivalence Model checkER. - David Hopkins 002; C.-H. Luke Ong (CAV, 2009)

Winning Regions of Pushdown Parity Games: A Saturation Method. - Matthew Hague; C.-H. Luke Ong (CONCUR, 2009)

On Global Model Checking Trees Generated by Higher-Order Recursion Schemes. - Christopher H. Broadbent; C.-H. Luke Ong (FoSSaCS, 2009)

A Type System Equivalent to the Modal Mu-Calculus Model Checking of Higher-Order Recursion Schemes. - Naoki Kobayashi 001; C.-H. Luke Ong (LICS, 2009)

Functional Reachability. - C.-H. Luke Ong; Nikos Tzevelekos (LICS, 2009)

The Safe Lambda Calculus - William Blum; C.-H. Luke Ong (Log. Methods Comput. Sci., 2009)

Recursion Schemes and Logical Reflection. - Christopher H. Broadbent; Arnaud Carayol; C.-H. Luke Ong; Olivier Serre (LICS, 2010)

Analysing Mu-Calculus Properties of Pushdown Systems. - Matthew Hague; C.-H. Luke Ong (SPIN, 2010)

Boom: Taking Boolean Program Model Checking One Step Further. - Gérard Basler; Matthew Hague; Daniel Kroening; C.-H. Luke Ong; Thomas Wahl; Haoxian Zhao (TACAS, 2010)

A Saturation Method for the Modal Mu-Calculus with Backwards Modalities over Pushdown Systems - Matthew Hague; C.-H. Luke Ong (CoRR, 2010)

Models of Higher-Order Computation: Recursion Schemes and Collapsible Pushdown Automata. - C.-H. Luke Ong (Logics and Languages for Reliability and Security, 2010)

A Fragment of ML Decidable by Visibly Pushdown Automata. - David Hopkins 002; Andrzej S. Murawski; C.-H. Luke Ong (ICALP (2), 2011)

Verifying higher-order functional programs with pattern-matching algebraic data types. - C.-H. Luke Ong; Steven J. Ramsay (POPL, 2011)

Improved Functional Flow and Reachability Analyses Using Indexed Linear Tree Grammars. - Jonathan Kochems; C.-H. Luke Ong (RTA, 2011)

Complexity of Model Checking Recursion Schemes for Fragments of the Modal Mu-Calculus - Naoki Kobayashi 001; C.-H. Luke Ong (Log. Methods Comput. Sci., 2011)

A saturation method for the modal μ-calculus over pushdown systems. - Matthew Hague; C.-H. Luke Ong (Inf. Comput., 2011)

Automated Techniques for Higher-Order Program Verification (NII Shonan Meeting 2011-5). - Naoki Kobayashi 001; Luke Ong; David Van Horn (NII Shonan Meet. Rep., 2011)

Soter: an automatic safety verifier for erlang. - Emanuele D'Osualdo; Jonathan Kochems; Luke Ong (AGERE!@SPLASH, 2012)

Hector: An Equivalence Checker for a Higher-Order Fragment of ML. - David Hopkins 002; Andrzej S. Murawski; C.-H. Luke Ong (CAV, 2012)

Two-Level Game Semantics, Intersection Types, and Recursion Schemes. - C.-H. Luke Ong; Takeshi Tsukada (ICALP (2), 2012)

A traversal-based algorithm for higher-order model checking. - Robin P. Neatherway; Steven J. Ramsay; C.-H. Luke Ong (ICFP, 2012)

Safety Verification of Asynchronous Pushdown Systems with Shaped Stacks. - Jonathan Kochems; C.-H. Luke Ong (CONCUR, 2013)

Recursion Schemes, Collapsible Pushdown Automata and Higher-Order Model Checking. - Luke Ong (LATA, 2013)

Automatic Verification of Erlang-Style Concurrency. - Emanuele D'Osualdo; Jonathan Kochems; C.-H. Luke Ong (SAS, 2013)

Information Flow Analysis for a Dynamically Typed Functional Language with Staged Metaprogramming - Martin Lester 001; C.-H. Luke Ong; Max Schäfer (CoRR, 2013)

Compositional higher-order model checking via ω-regular games over Böhm trees. - Takeshi Tsukada; C.-H. Luke Ong (CSL-LICS, 2014)

EGuaranteeNash for Boolean Games Is NEXP-Hard. - Egor Ianovski; Luke Ong (KR, 2014)

A type-directed abstraction refinement approach to higher-order model checking. - Steven J. Ramsay; Robin P. Neatherway; C.-H. Luke Ong (POPL, 2014)

TravMC2: higher-order model checking for alternating parity tree automata. - Robin P. Neatherway; C.-H. Luke Ong (SPIN, 2014)

Decidable Models of Recursive Asynchronous Concurrency. - Jonathan Kochems; C.-H. Luke Ong (CoRR, 2014)

Innocent Strategies are Sheaves over Plays - Deterministic, Non-deterministic and Probabilistic Innocence. - Takeshi Tsukada; C.-H. Luke Ong (CoRR, 2014)

Fragments of ML Decidable by Nested Data Class Memory Automata. - Conrad Cotton-Barratt; David Hopkins 002; Andrzej S. Murawski; C.-H. Luke Ong (FoSSaCS, 2015)

Weak and Nested Class Memory Automata. - Conrad Cotton-Barratt; Andrzej S. Murawski; C.-H. Luke Ong (LATA, 2015)

Higher-Order Model Checking: An Overview. - Luke Ong (LICS, 2015)

Nondeterminism in Game Semantics via Sheaves. - Takeshi Tsukada; C.-H. Luke Ong (LICS, 2015)

Detecting redundant CSS rules in HTML5 applications: a tree rewriting approach. - Matthew Hague; Anthony Widjaja Lin; C.-H. Luke Ong (OOPSLA, 2015)

A Type System for proving Depth Boundedness in the pi-calculus. - Emanuele D'Osualdo; Luke Ong (CoRR, 2015)

Unboundedness and Downwards Closures of Higher-Order Pushdown Automata. - Matthew Hague; Jonathan Kochems; C.-H. Luke Ong (CoRR, 2015)

Normalisation by Traversals. - C.-H. Luke Ong (CoRR, 2015)

Logic, Language, Information and Computation (WoLLIC 2012). - C.-H. Luke Ong; Ruy J. G. B. de Queiroz (Theor. Comput. Sci., 2015)

On Hierarchical Communication Topologies in the pi -calculus. - Emanuele D'Osualdo; C.-H. Luke Ong (ESOP, 2016)

Plays as Resource Terms via Non-idempotent Intersection Types. - Takeshi Tsukada; C.-H. Luke Ong (LICS, 2016)

Unboundedness and downward closures of higher-order pushdown automata. - Matthew Hague; Jonathan Kochems; C.-H. Luke Ong (POPL, 2016)

Information flow analysis for a dynamically typed language with staged metaprogramming. - Martin Mariusz Lester; Luke Ong; Max Schäfer (J. Comput. Secur., 2016)

Higher-Order Model Checking (NII Shonan Meeting 2016-4). - Naoki Kobayashi 001; Luke Ong; Igor Walukiewicz (NII Shonan Meet. Rep., 2016)

Deciding Secrecy of Security Protocols for an Unbounded Number of Sessions: The Case of Depth-Bounded Processes. - Emanuele D'Osualdo; Luke Ong; Alwen Tiu (CSF, 2017)

ML and Extended Branching VASS. - Conrad Cotton-Barratt; Andrzej S. Murawski; C.-H. Luke Ong (ESOP, 2017)

Automata, Logic and Games for the λ-Calculus. - C.-H. Luke Ong (ICLA, 2017)

More effective interpolations in software model checking. - Cong Tian; Zhao Duan; Zhenhua Duan; C.-H. Luke Ong (ASE, 2017)

Quantitative semantics of the lambda calculus: Some generalisations of the relational model. - C.-H. Luke Ong (LICS, 2017)

Generalised species of rigid resource terms. - Takeshi Tsukada; Kazuyuki Asada; C.-H. Luke Ong (LICS, 2017)

Higher-Order Constrained Horn Clauses and Refinement Types. - Toby Cathcart Burn; C.-H. Luke Ong; Steven J. Ramsay (CoRR, 2017)

Collapsible Pushdown Automata and Recursion Schemes. - Matthew Hague; Andrzej S. Murawski; C.-H. Luke Ong; Olivier Serre (ACM Trans. Comput. Log., 2017)

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 (LICS, 2018)

InterpChecker: Reducing State Space via Interpolations - (Competition Contribution). - Zhao Duan; Cong Tian; Zhenhua Duan; C.-H. Luke Ong (TACAS (2), 2018)

The complexity of decision problems about equilibria in two-player Boolean games. - Egor Ianovski; Luke Ong (Artif. Intell., 2018)

Defunctionalization of Higher-Order Constrained Horn Clauses. - Long Pham; Steven J. Ramsay; C.-H. Luke Ong (CoRR, 2018)

Simulating cardinal preferences in Boolean games: A proof technique. - Egor Ianovski; Luke Ong (Inf. Comput., 2018)

Higher-order constrained horn clauses for verification. - Toby Cathcart Burn; C.-H. Luke Ong; Steven J. Ramsay (Proc. ACM Program. Lang., 2018)

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 (ESOP, 2019)

Change Actions: Models of Generalised Differentiation. - Mario Alvarez-Picallo; C.-H. Luke Ong (FoSSaCS, 2019)

Typed Meta-interpretive Learning of Logic Programs. - Rolf Morel; Andrew Cropper; C.-H. Luke Ong (JELIA, 2019)

HoCHC: A Refutationally Complete and Semantically Invariant System of Higher-order Logic Modulo Theories. - C.-H. Luke Ong; Dominik Wagner 001 (LICS, 2019)

Polynomial Probabilistic Invariants and the Optional Stopping Theorem. - Anne Schreuder; C.-H. Luke Ong (CoRR, 2019)

ML, Visibly Pushdown Class Memory Automata, and Extended Branching Vector Addition Systems with States. - Conrad Cotton-Barratt; Andrzej S. Murawski; C.-H. Luke Ong (ACM Trans. Program. Lang. Syst., 2019)

The Difference λ-Calculus: A Language for Difference Categories. - Mario Alvarez-Picallo; C.-H. Luke Ong (FSCD, 2020)

A Differential-form Pullback Programming Language for Higher-order Reverse-mode Automatic Differentiation. - Carol Mak; Luke Ong (CoRR, 2020)

The Extended Theory of Trees and Algebraic (Co)datatypes. - Fabian Zaiser; C.-H. Luke Ong (VPT/HCVS@ETAPS, 2020)

The Difference Lambda-Calculus: A Language for Difference Categories. - Mario Alvarez-Picallo; C.-H. Luke Ong (CoRR, 2020)

Verifying Liveness Properties of ML Programs. - Martin Lester 001; Robin P. Neatherway; C.-H. Luke Ong; Steven J. Ramsay (CoRR, 2020)

Densities of Almost Surely Terminating Probabilistic Programs are Differentiable Almost Everywhere. - Carol Mak; C.-H. Luke Ong; Hugo Paquet; Dominik Wagner 001 (ESOP, 2021)

Nonparametric Hamiltonian Monte Carlo. - Carol Mak; Fabian Zaiser; Luke Ong (ICML, 2021)

Initial Limit Datalog: a New Extensible Class of Decidable Constrained Horn Clauses. - Toby Cathcart Burn; Luke Ong; Steven J. Ramsay; Dominik Wagner 001 (LICS, 2021)

Supermartingales, Ranking Functions and Probabilistic Lambda Calculus. - Andrew Kenyon-Roberts; C.-H. Luke Ong (LICS, 2021)

On probabilistic termination of functional programs with continuous distributions. - Raven Beutner; Luke Ong (PLDI, 2021)

Abstract: The Extended Theory of Trees and Algebraic (Co)datatypes. - Fabian Zaiser; Luke Ong (SMT, 2021)

Expectation Programming. - Tim Reichelt; Adam Golinski; Luke Ong; Tom Rainforth (CoRR, 2021)

Collapsible Pushdown Parity Games. - Christopher H. Broadbent; Arnaud Carayol; Matthew Hague; Andrzej S. Murawski; C.-H. Luke Ong; Olivier Serre (ACM Trans. Comput. Log., 2021)

Higher-order Recursion Schemes and Collapsible Pushdown Automata: Logical Properties. - Christopher H. Broadbent; Arnaud Carayol; C.-H. Luke Ong; Olivier Serre (ACM Trans. Comput. Log., 2021)

Nonparametric Involutive Markov Chain Monte Carlo. - Carol Mak; Fabian Zaiser; Luke Ong (ICML, 2022)

Probabilistic Verification Beyond Context-Freeness. - Guanyan Li; Andrzej S. Murawski; Luke Ong (LICS, 2022)

Rethinking Variational Inference for Probabilistic Programs with Stochastic Support. - Tim Reichelt; Luke Ong; Thomas Rainforth (NeurIPS, 2022)

Guaranteed bounds for posterior inference in universal probabilistic programming. - Raven Beutner; C.-H. Luke Ong; Fabian Zaiser (PLDI, 2022)

CycleQ: an efficient basis for cyclic equational reasoning. - Eddie Jones; C.-H. Luke Ong; Steven J. Ramsay (PLDI, 2022)

Expectation programming: Adapting probabilistic programming systems to estimate expectations efficiently. - Tim Reichelt; Adam Golinski; Luke Ong; Tom Rainforth (UAI, 2022)

Artifact for: Rigorous bounds for posterior inference in universal probabilistic programming (PLDI 2022). - Raven Beutner; Luke Ong; Fabian Zaiser (Zenodo, 2022)

Artifact for: Rigorous bounds for posterior inference in universal probabilistic programming (PLDI 2022). - Raven Beutner; Luke Ong; Fabian Zaiser (Zenodo, 2022)

Artifact for: Guaranteed Bounds for Posterior Inference in Universal Probabilistic Programming (PLDI 2022). - Raven Beutner; Luke Ong; Fabian Zaiser (Zenodo, 2022)

Fast and Correct Gradient-Based Optimisation for Probabilistic Programming via Smoothing. - Basim Khajwal; C.-H. Luke Ong; Dominik Wagner 001 (ESOP, 2023)

Exact Bayesian Inference on Discrete Models via Probability Generating Functions: A Probabilistic Programming Approach. - Fabian Zaiser; Andrzej S. Murawski; Chih-Hao Luke Ong (NeurIPS, 2023)

PTSV: Probabilistic Tree-Stack Verifier. - Guanyan Li; Andrzej S. Murawski; Luke Ong (Zenodo, 2023)

Template-Based Static Posterior Inference for Bayesian Probabilistic Programming. - Peixin Wang; Hongfei Fu 001; Tengshun Yang; Guanyan Li; Luke Ong (CoRR, 2023)

PTSV: Probabilistic Tree-Stack Verifier. - Guanyan Li; Andrzej S. Murawski; Luke Ong (Zenodo, 2023)

Beyond Bayesian Model Averaging over Paths in Probabilistic Programs with Stochastic Support. - Tim Reichelt; Luke Ong; Tom Rainforth (AISTATS, 2024)

Diagonalisation SGD: Fast & Convergent SGD for Non-Differentiable Models via Reparameterisation and Smoothing. - Dominik Wagner 001; Basim Khajwal; Luke Ong (AISTATS, 2024)

Unifying Qualitative and Quantitative Safety Verification of DNN-Controlled Systems. - Dapeng Zhi; Peixin Wang; Si Liu 003; C.-H. Luke Ong; Min Zhang 002 (CAV (2), 2024)

Reinforcement Learning with LTL and ω-Regular Objectives via Optimality-Preserving Translation to Average Rewards. - Xuan-Bach Le; Dominik Wagner 001; Leon Witzman; Alexander Rabinovich; Luke Ong (NeurIPS, 2024)

Static Posterior Inference of Bayesian Probabilistic Programming via Polynomial Solving. - Peixin Wang; Tengshun Yang; Hongfei Fu 001; Guanyan Li; C.-H. Luke Ong (Proc. ACM Program. Lang., 2024)

Towards Interpreting Visual Information Processing in Vision-Language Models. - Clement Neo; Luke Ong; Philip Torr 001; Mor Geva; David Krueger 001; Fazl Barez (ICLR, 2025)

Guaranteed Bounds on Posterior Distributions of Discrete Probabilistic Programs with Loops. - Fabian Zaiser; Andrzej S. Murawski; C.-H. Luke Ong (Proc. ACM Program. Lang., 2025)

Open Problems in Machine Unlearning for AI Safety. - Fazl Barez; Tingchen Fu; Ameya Prabhu; Stephen Casper; Amartya Sanyal; Adel Bibi; Aidan O'Gara; Robert Kirk; Ben Bucknall; Timothy Fist; Luke Ong; Philip Torr 001; et al. (CoRR, 2025)

The Singapore Consensus on Global AI Safety Research Priorities. - Yoshua Bengio; Tegan Maharaj; Luke Ong; Stuart Russell 001; Dawn Song; Max Tegmark; Lan Xue; Ya-Qin Zhang; Stephen Casper; Wan Sie Lee; Sören Mindermann; Vanessa Wilfred; et al. (CoRR, 2025)

Conformal Prediction Meets Long-tail Classification. - Shuqi Liu; Jianguo Huang; Luke Ong (CoRR, 2025)