C.-H. Luke Ong

ORCID

Publication Activity (10 Years)

Years Active: 1988-2024
Publications (10 Years): 43

Top Venues

CoRR

LICS

ESOP

ACM Trans. Comput. Log.

Publications

Dominik Wagner, Basim Khajwal, C.-H. Luke Ong
Diagonalisation SGD: Fast & Convergent SGD for Non-Differentiable Models via Reparameterisation and Smoothing. CoRR (2024)
Dapeng Zhi, Peixin Wang, Si Liu, C.-H. Luke Ong, Min Zhang
Unifying Qualitative and Quantitative Safety Verification of DNN-Controlled Systems. CAV (2) (2024)
Peixin Wang, Tengshun Yang, Hongfei Fu, Guanyan Li, C.-H. Luke Ong
Static Posterior Inference of Bayesian Probabilistic Programming via Polynomial Solving. Proc. ACM Program. Lang. 8 (PLDI) (2024)
Basim Khajwal, C.-H. Luke Ong, Dominik Wagner
Fast and Correct Gradient-Based Optimisation for Probabilistic Programming via Smoothing. ESOP (2023)
Basim Khajwal, C.-H. Luke Ong, Dominik Wagner
Fast and Correct Gradient-Based Optimisation for Probabilistic Programming via Smoothing. CoRR (2023)
Eddie Jones, C.-H. Luke Ong, Steven J. Ramsay
CycleQ: an efficient basis for cyclic equational reasoning. PLDI (2022)
Raven Beutner, C.-H. Luke Ong, Fabian Zaiser
Guaranteed bounds for posterior inference in universal probabilistic programming. PLDI (2022)
Andrew Kenyon-Roberts, C.-H. Luke Ong
Supermartingales, Ranking Functions and Probabilistic Lambda Calculus. LICS (2021)
Eddie Jones, C.-H. Luke Ong, Steven J. Ramsay
CycleQ: An Efficient Basis for Cyclic Equational Reasoning. CoRR (2021)
Christopher H. Broadbent, Arnaud Carayol, C.-H. Luke Ong, Olivier Serre
Higher-order Recursion Schemes and Collapsible Pushdown Automata: Logical Properties. ACM Trans. Comput. Log. 22 (2) (2021)
Carol Mak, C.-H. Luke Ong, Hugo Paquet, Dominik Wagner
Densities of Almost Surely Terminating Probabilistic Programs are Differentiable Almost Everywhere. ESOP (2021)
Christopher H. Broadbent, Arnaud Carayol, Matthew Hague, Andrzej S. Murawski, C.-H. Luke Ong, Olivier Serre
Collapsible Pushdown Parity Games. ACM Trans. Comput. Log. 22 (3) (2021)
Christopher H. Broadbent, Arnaud Carayol, C.-H. Luke Ong, Olivier Serre
Higher-Order Recursion Schemes and Collapsible Pushdown Automata: Logical Properties. CoRR (2020)
Martin Lester, Robin P. Neatherway, C.-H. Luke Ong, Steven J. Ramsay
Verifying Liveness Properties of ML Programs. CoRR (2020)
Fabian Zaiser, C.-H. Luke Ong
The Extended Theory of Trees and Algebraic (Co)datatypes. VPT/HCVS@ETAPS (2020)
Mario Alvarez-Picallo, C.-H. Luke Ong
The Difference λ-Calculus: A Language for Difference Categories. FSCD (2020)
Carol Mak, C.-H. Luke Ong, Hugo Paquet, Dominik Wagner
Densities of almost-surely terminating probabilistic programs are differentiable almost everywhere. CoRR (2020)
Mario Alvarez-Picallo, C.-H. Luke Ong
The Difference Lambda-Calculus: A Language for Difference Categories. CoRR (2020)
Christopher H. Broadbent, Arnaud Carayol, Matthew Hague, Andrzej S. Murawski, C.-H. Luke Ong, Olivier Serre
Collapsible Pushdown Parity Games. CoRR (2020)
C.-H. Luke Ong, Dominik Wagner
HoCHC: a Refutationally-complete and Semantically-invariant System of Higher-order Logic Modulo Theories. CoRR (2019)
Mario Alvarez-Picallo, C.-H. Luke Ong
Change Actions: Models of Generalised Differentiation. FoSSaCS (2019)
C.-H. Luke Ong, Dominik Wagner
HoCHC: A Refutationally Complete and Semantically Invariant System of Higher-order Logic Modulo Theories. LICS (2019)
Rolf Morel, Andrew Cropper, C.-H. Luke Ong
Typed Meta-interpretive Learning of Logic Programs. JELIA (2019)
Mario Alvarez-Picallo, C.-H. Luke Ong
Change Actions: Models of Generalised Differentiation. CoRR (2019)
Mario Alvarez-Picallo, Alex Eyers-Taylor, Michael Peyton Jones, C.-H. Luke Ong
Fixing Incremental Computation - Derivatives of Fixpoints, and the Recursive Semantics of Datalog. ESOP (2019)
Conrad Cotton-Barratt, Andrzej S. Murawski, C.-H. Luke Ong
ML, Visibly Pushdown Class Memory Automata, and Extended Branching Vector Addition Systems with States. ACM Trans. Program. Lang. Syst. 41 (2) (2019)
Anne Schreuder, C.-H. Luke Ong
Polynomial Probabilistic Invariants and the Optional Stopping Theorem. CoRR (2019)
Toby Cathcart Burn, C.-H. Luke Ong, Steven J. Ramsay
Higher-order constrained horn clauses for verification. Proc. ACM Program. Lang. 2 (POPL) (2018)
Long Pham, Steven J. Ramsay, C.-H. Luke Ong
Defunctionalization of Higher-Order Constrained Horn Clauses. CoRR (2018)
Zhao Duan, Cong Tian, Zhenhua Duan, C.-H. Luke Ong
InterpChecker: Reducing State Space via Interpolations - (Competition Contribution). TACAS (2) (2018)
Mario Alvarez-Picallo, Alex Eyers-Taylor, Michael Peyton Jones, C.-H. Luke Ong
Fixing Incremental Computation: Derivatives of Fixpoints, and the Recursive Semantics of Datalog. CoRR (2018)
Takeshi Tsukada, Kazuyuki Asada, C.-H. Luke Ong
Species, Profunctors and Taylor Expansion Weighted by SMCC: A Unified Framework for Modelling Nondeterministic, Probabilistic and Quantum Programs. LICS (2018)
C.-H. Luke Ong
Quantitative semantics of the lambda calculus: Some generalisations of the relational model. LICS (2017)
Matthew Hague, Andrzej S. Murawski, C.-H. Luke Ong, Olivier Serre
Collapsible Pushdown Automata and Recursion Schemes. ACM Trans. Comput. Log. 18 (3) (2017)
Takeshi Tsukada, Kazuyuki Asada, C.-H. Luke Ong
Generalised species of rigid resource terms. LICS (2017)
C.-H. Luke Ong
Automata, Logic and Games for the λ-Calculus. ICLA (2017)
Conrad Cotton-Barratt, Andrzej S. Murawski, C.-H. Luke Ong
ML and Extended Branching VASS. ESOP (2017)
Toby Cathcart Burn, C.-H. Luke Ong, Steven J. Ramsay
Higher-Order Constrained Horn Clauses and Refinement Types. CoRR (2017)
Cong Tian, Zhao Duan, Zhenhua Duan, C.-H. Luke Ong
More effective interpolations in software model checking. ASE (2017)
Takeshi Tsukada, C.-H. Luke Ong
Plays as Resource Terms via Non-idempotent Intersection Types. LICS (2016)
Emanuele D'Osualdo, C.-H. Luke Ong
On Hierarchical Communication Topologies in the \pi -calculus. ESOP (2016)
Matthew Hague, Jonathan Kochems, C.-H. Luke Ong
Unboundedness and downward closures of higher-order pushdown automata. POPL (2016)
Emanuele D'Osualdo, C.-H. Luke Ong
On Hierarchical Communication Topologies in the pi-calculus. CoRR (2016)
C.-H. Luke Ong
Normalisation by Traversals. CoRR (2015)
Takeshi Tsukada, C.-H. Luke Ong
Nondeterminism in Game Semantics via Sheaves. LICS (2015)
Conrad Cotton-Barratt, David Hopkins, Andrzej S. Murawski, C.-H. Luke Ong
Fragments of ML Decidable by Nested Data Class Memory Automata. CoRR (2015)
C.-H. Luke Ong, Ruy J. G. B. de Queiroz
Logic, Language, Information and Computation (WoLLIC 2012). Theor. Comput. Sci. 603 (2015)
Matthew Hague, Anthony Widjaja Lin, C.-H. Luke Ong
Detecting redundant CSS rules in HTML5 applications: a tree rewriting approach. OOPSLA (2015)
Conrad Cotton-Barratt, David Hopkins, Andrzej S. Murawski, C.-H. Luke Ong
Fragments of ML Decidable by Nested Data Class Memory Automata. FoSSaCS (2015)
Matthew Hague, Jonathan Kochems, C.-H. Luke Ong
Unboundedness and Downwards Closures of Higher-Order Pushdown Automata. CoRR (2015)
Conrad Cotton-Barratt, Andrzej S. Murawski, C.-H. Luke Ong
Weak and Nested Class Memory Automata. LATA (2015)
Steven J. Ramsay, Robin P. Neatherway, C.-H. Luke Ong
A type-directed abstraction refinement approach to higher-order model checking. POPL (2014)
Takeshi Tsukada, C.-H. Luke Ong
Innocent Strategies are Sheaves over Plays - Deterministic, Non-deterministic and Probabilistic Innocence. CoRR (2014)
Conrad Cotton-Barratt, Andrzej S. Murawski, C.-H. Luke Ong
Weak and Nested Class Memory Automata. CoRR (2014)
Jonathan Kochems, C.-H. Luke Ong
Decidable Models of Recursive Asynchronous Concurrency. CoRR (2014)
Robin P. Neatherway, C.-H. Luke Ong
TravMC2: higher-order model checking for alternating parity tree automata. SPIN (2014)
Takeshi Tsukada, C.-H. Luke Ong
-regular games over Böhm trees. CSL-LICS (2014)
Jonathan Kochems, C.-H. Luke Ong
Safety verification of asynchronous pushdown systems with shaped stacks. CoRR (2014)
Emanuele D'Osualdo, Jonathan Kochems, C.-H. Luke Ong
Automatic Verification of Erlang-Style Concurrency CoRR (2013)
Jonathan Kochems, C.-H. Luke Ong
Safety Verification of Asynchronous Pushdown Systems with Shaped Stacks. CONCUR (2013)
Emanuele D'Osualdo, Jonathan Kochems, C.-H. Luke Ong
Automatic Verification of Erlang-Style Concurrency. SAS (2013)
Martin Lester, C.-H. Luke Ong, Max Schäfer
Information Flow Analysis for a Dynamically Typed Functional Language with Staged Metaprogramming CoRR (2013)
C.-H. Luke Ong, Takeshi Tsukada
Two-Level Game Semantics, Intersection Types, and Recursion Schemes. ICALP (2) (2012)
Robin P. Neatherway, Steven J. Ramsay, C.-H. Luke Ong
A traversal-based algorithm for higher-order model checking. ICFP (2012)
David Hopkins, Andrzej S. Murawski, C.-H. Luke Ong
Hector: An Equivalence Checker for a Higher-Order Fragment of ML. CAV (2012)
David Hopkins, Andrzej S. Murawski, C.-H. Luke Ong
A Fragment of ML Decidable by Visibly Pushdown Automata. ICALP (2) (2011)
C.-H. Luke Ong, Steven J. Ramsay
Verifying higher-order functional programs with pattern-matching algebraic data types. POPL (2011)
Naoki Kobayashi, C.-H. Luke Ong
Complexity of Model Checking Recursion Schemes for Fragments of the Modal Mu-Calculus Log. Methods Comput. Sci. 7 (4) (2011)
Matthew Hague, C.-H. Luke Ong
A saturation method for the modal μ-calculus over pushdown systems. Inf. Comput. 209 (5) (2011)
Jonathan Kochems, C.-H. Luke Ong
Improved Functional Flow and Reachability Analyses Using Indexed Linear Tree Grammars. RTA (2011)
Gérard Basler, Matthew Hague, Daniel Kroening, C.-H. Luke Ong, Thomas Wahl, Haoxian Zhao
Boom: Taking Boolean Program Model Checking One Step Further. TACAS (2010)
Christopher H. Broadbent, Arnaud Carayol, C.-H. Luke Ong, Olivier Serre
Recursion Schemes and Logical Reflection. LICS (2010)
Matthew Hague, C.-H. Luke Ong
Analysing Mu-Calculus Properties of Pushdown Systems. SPIN (2010)
Matthew Hague, C.-H. Luke Ong
A Saturation Method for the Modal Mu-Calculus with Backwards Modalities over Pushdown Systems CoRR (2010)
Christopher H. Broadbent, C.-H. Luke Ong
On Global Model Checking Trees Generated by Higher-Order Recursion Schemes. FoSSaCS (2009)
William Blum, C.-H. Luke Ong
The Safe Lambda Calculus Log. Methods Comput. Sci. 5 (1) (2009)
Naoki Kobayashi, C.-H. Luke Ong
Complexity of Model Checking Recursion Schemes for Fragments of the Modal Mu-Calculus. ICALP (2) (2009)
Naoki Kobayashi, C.-H. Luke Ong
A Type System Equivalent to the Modal Mu-Calculus Model Checking of Higher-Order Recursion Schemes. LICS (2009)
Matthew Hague, C.-H. Luke Ong
Winning Regions of Pushdown Parity Games: A Saturation Method. CONCUR (2009)
David Hopkins, C.-H. Luke Ong
Homer: A Higher-Order Observational Equivalence Model checkER. CAV (2009)
C.-H. Luke Ong, Nikos Tzevelekos
Functional Reachability. LICS (2009)
Arnaud Carayol, Matthew Hague, Antoine Meyer, C.-H. Luke Ong, Olivier Serre
Winning Regions of Higher-Order Pushdown Games. LICS (2008)
Matthew Hague, C.-H. Luke Ong
Symbolic Backwards-Reachability Analysis for Higher-Order Pushdown Systems. Log. Methods Comput. Sci. 4 (4) (2008)
Matthew Hague, C.-H. Luke Ong
Symbolic Backwards-Reachability Analysis for Higher-Order Pushdown Systems CoRR (2008)
Matthew Hague, Andrzej S. Murawski, C.-H. Luke Ong, Olivier Serre
Collapsible Pushdown Automata and Recursion Schemes. LICS (2008)
C.-H. Luke Ong
Verification of Higher-Order Computation: A Game-Semantic Approach. ESOP (2008)
S. B. Sanjabi, C.-H. Luke Ong
Fully abstract semantics of additive aspects by translation. AOSD (2007)
Matthew Hague, C.-H. Luke Ong
Symbolic Backwards-Reachability Analysis for Higher-Order Pushdown Systems. FoSSaCS (2007)
C.-H. Luke Ong
Hierarchies of Infinite Structures Generated by Pushdown Automata and Recursion Schemes. MFCS (2007)
William Blum, C.-H. Luke Ong
The Safe Lambda Calculus. TLCA (2007)
Andrzej S. Murawski, C.-H. Luke Ong
Fast verification of MLL proof nets via IMLL. ACM Trans. Comput. Log. 7 (3) (2006)
C.-H. Luke Ong
On Model-Checking Trees Generated by Higher-Order Recursion Schemes. LICS (2006)
Dan R. Ghica, Andrzej S. Murawski, C.-H. Luke Ong
Syntactic control of concurrency. Theor. Comput. Sci. 350 (2-3) (2006)
C.-H. Luke Ong
Some Results on a Game-Semantic Approach to Verifying Finitely-Presentable Infinite Structures (Extended Abstract). CSL (2006)
Klaus Aehlig, Jolie G. de Miranda, C.-H. Luke Ong
Safety Is not a Restriction at Level 2 for String Languages. FoSSaCS (2005)
Klaus Aehlig, Jolie G. de Miranda, C.-H. Luke Ong
The Monadic Second Order Theory of Trees Given by Arbitrary Level-Two Recursion Schemes Is Decidable. TLCA (2005)
Andrzej S. Murawski, C.-H. Luke Ong, Igor Walukiewicz
Idealized Algol with Ground Recursion, and DPDA Equivalence. ICALP (2005)
Samson Abramsky, Dan R. Ghica, Andrzej S. Murawski, C.-H. Luke Ong, Ian David Bede Stark
Nominal Games and Full Abstraction for the Nu-Calculus. LICS (2004)
C.-H. Luke Ong
An approach to deciding the observational equivalence of Algol-like languages. Ann. Pure Appl. Log. 130 (1-3) (2004)
Samson Abramsky, Dan R. Ghica, Andrzej S. Murawski, C.-H. Luke Ong
Applying Game Semantics to Compositional Software Modeling and Verification. TACAS (2004)

C.-H. Luke Ong.css-eqlu8i{font-size:small;padding-left:4px;}

Publication Activity (10 Years)

Top Topics

Top Venues

C.-H. Luke Ong