C.-H. Luke Ong

138 papers A* 32A 10B 18C 2Misc 1Journal 52Unranked 20

Year	Rank	Type	Title / Venue / Authors
2026	J	`jnl`	Layered Modal ML: Syntax and Full Abstraction. CoRR Haoxuan Yin, Andrzej S. Murawski, C.-H. Luke Ong
2026	J	`jnl`	PAC Finite-Time Safety Guarantees for Stochastic Systems with Unknown Disturbance Distributions. CoRR Taoran Wu, Dominik Wagner, C.-H. Luke Ong, Bai Xue
2025	J	`jnl`	Guaranteed Bounds on Posterior Distributions of Discrete Probabilistic Programs with Loops. Proc. ACM Program. Lang. Fabian Zaiser, Andrzej S. Murawski, C.-H. Luke Ong
2025	J	`jnl`	Quantitative Verification of Omega-regular Properties in Probabilistic Programming. CoRR Peixin Wang, Jianhao Bai, Min Zhang, C.-H. Luke Ong
2024	J	`jnl`	Diagonalisation SGD: Fast & Convergent SGD for Non-Differentiable Models via Reparameterisation and Smoothing. CoRR Dominik Wagner, Basim Khajwal, C.-H. Luke Ong
2024	J	`jnl`	Guaranteed Bounds on Posterior Distributions of Discrete Probabilistic Programs with Loops. CoRR Fabian Zaiser, Andrzej S. Murawski, C.-H. Luke Ong
2024	J	`jnl`	Static Posterior Inference of Bayesian Probabilistic Programming via Polynomial Solving. Proc. ACM Program. Lang. Peixin Wang, Tengshun Yang, Hongfei Fu, Guanyan Li, C.-H. Luke Ong
2024	—	`conf`	Unifying Qualitative and Quantitative Safety Verification of DNN-Controlled Systems. CAV (2) Dapeng Zhi, Peixin Wang, Si Liu, C.-H. Luke Ong, Min Zhang
2023	A	`conf`	Fast and Correct Gradient-Based Optimisation for Probabilistic Programming via Smoothing. ESOP Basim Khajwal, C.-H. Luke Ong, Dominik Wagner
2023	J	`jnl`	Fast and Correct Gradient-Based Optimisation for Probabilistic Programming via Smoothing. CoRR Basim Khajwal, C.-H. Luke Ong, Dominik Wagner
2022	A*	`conf`	CycleQ: an efficient basis for cyclic equational reasoning. PLDI Eddie Jones, C.-H. Luke Ong, Steven J. Ramsay
2022	A*	`conf`	Guaranteed bounds for posterior inference in universal probabilistic programming. PLDI Raven Beutner, C.-H. Luke Ong, Fabian Zaiser
2021	J	`jnl`	Collapsible Pushdown Parity Games. ACM Trans. Comput. Log. Christopher H. Broadbent, Arnaud Carayol, Matthew Hague, Andrzej S. Murawski, C.-H. Luke Ong, Olivier Serre
2021	J	`jnl`	CycleQ: An Efficient Basis for Cyclic Equational Reasoning. CoRR Eddie Jones, C.-H. Luke Ong, Steven J. Ramsay
2021	A	`conf`	Densities of Almost Surely Terminating Probabilistic Programs are Differentiable Almost Everywhere. ESOP Carol Mak, C.-H. Luke Ong, Hugo Paquet, Dominik Wagner
2021	J	`jnl`	Higher-order Recursion Schemes and Collapsible Pushdown Automata: Logical Properties. ACM Trans. Comput. Log. Christopher H. Broadbent, Arnaud Carayol, C.-H. Luke Ong, Olivier Serre
2021	A*	`conf`	Supermartingales, Ranking Functions and Probabilistic Lambda Calculus. LICS Andrew Kenyon-Roberts, C.-H. Luke Ong
2020	J	`jnl`	Collapsible Pushdown Parity Games. CoRR Christopher H. Broadbent, Arnaud Carayol, Matthew Hague, Andrzej S. Murawski, C.-H. Luke Ong, Olivier Serre
2020	J	`jnl`	Densities of almost-surely terminating probabilistic programs are differentiable almost everywhere. CoRR Carol Mak, C.-H. Luke Ong, Hugo Paquet, Dominik Wagner
2020	J	`jnl`	Higher-Order Recursion Schemes and Collapsible Pushdown Automata: Logical Properties. CoRR Christopher H. Broadbent, Arnaud Carayol, C.-H. Luke Ong, Olivier Serre
2020	J	`jnl`	The Difference Lambda-Calculus: A Language for Difference Categories. CoRR Mario Alvarez-Picallo, C.-H. Luke Ong
2020	B	`conf`	The Difference λ-Calculus: A Language for Difference Categories. FSCD Mario Alvarez-Picallo, C.-H. Luke Ong
2020	—	`conf`	The Extended Theory of Trees and Algebraic (Co)datatypes. VPT/HCVS@ETAPS Fabian Zaiser, C.-H. Luke Ong
2020	J	`jnl`	Verifying Liveness Properties of ML Programs. CoRR Martin Lester, Robin P. Neatherway, C.-H. Luke Ong, Steven J. Ramsay
2019	B	`conf`	Change Actions: Models of Generalised Differentiation. FoSSaCS Mario Alvarez-Picallo, C.-H. Luke Ong
2019	J	`jnl`	Change Actions: Models of Generalised Differentiation. CoRR Mario Alvarez-Picallo, C.-H. Luke Ong
2019	A	`conf`	Fixing Incremental Computation - Derivatives of Fixpoints, and the Recursive Semantics of Datalog. ESOP Mario Alvarez-Picallo, Alex Eyers-Taylor, Michael Peyton Jones, C.-H. Luke Ong
2019	A*	`conf`	HoCHC: A Refutationally Complete and Semantically Invariant System of Higher-order Logic Modulo Theories. LICS C.-H. Luke Ong, Dominik Wagner
2019	J	`jnl`	HoCHC: a Refutationally-complete and Semantically-invariant System of Higher-order Logic Modulo Theories. CoRR C.-H. Luke Ong, Dominik Wagner
2019	J	`jnl`	ML, Visibly Pushdown Class Memory Automata, and Extended Branching Vector Addition Systems with States. ACM Trans. Program. Lang. Syst. Conrad Cotton-Barratt, Andrzej S. Murawski, C.-H. Luke Ong
2019	J	`jnl`	Polynomial Probabilistic Invariants and the Optional Stopping Theorem. CoRR Anne Schreuder, C.-H. Luke Ong
2019	B	`conf`	Typed Meta-interpretive Learning of Logic Programs. JELIA Rolf Morel, Andrew Cropper, C.-H. Luke Ong
2018	J	`jnl`	Defunctionalization of Higher-Order Constrained Horn Clauses. CoRR Long Pham, Steven J. Ramsay, C.-H. Luke Ong
2018	J	`jnl`	Fixing Incremental Computation: Derivatives of Fixpoints, and the Recursive Semantics of Datalog. CoRR Mario Alvarez-Picallo, Alex Eyers-Taylor, Michael Peyton Jones, C.-H. Luke Ong
2018	J	`jnl`	Higher-order constrained horn clauses for verification. Proc. ACM Program. Lang. Toby Cathcart Burn, C.-H. Luke Ong, Steven J. Ramsay
2018	—	`conf`	InterpChecker: Reducing State Space via Interpolations - (Competition Contribution). TACAS (2) Zhao Duan, Cong Tian, Zhenhua Duan, C.-H. Luke Ong
2018	A*	`conf`	Species, Profunctors and Taylor Expansion Weighted by SMCC: A Unified Framework for Modelling Nondeterministic, Probabilistic and Quantum Programs. LICS Takeshi Tsukada, Kazuyuki Asada, C.-H. Luke Ong
2017	—	`conf`	Automata, Logic and Games for the λ-Calculus. ICLA C.-H. Luke Ong
2017	J	`jnl`	Collapsible Pushdown Automata and Recursion Schemes. ACM Trans. Comput. Log. Matthew Hague, Andrzej S. Murawski, C.-H. Luke Ong, Olivier Serre
2017	A*	`conf`	Generalised species of rigid resource terms. LICS Takeshi Tsukada, Kazuyuki Asada, C.-H. Luke Ong
2017	J	`jnl`	Higher-Order Constrained Horn Clauses and Refinement Types. CoRR Toby Cathcart Burn, C.-H. Luke Ong, Steven J. Ramsay
2017	A	`conf`	ML and Extended Branching VASS. ESOP Conrad Cotton-Barratt, Andrzej S. Murawski, C.-H. Luke Ong
2017	A*	`conf`	More effective interpolations in software model checking. ASE Cong Tian, Zhao Duan, Zhenhua Duan, C.-H. Luke Ong
2017	A*	`conf`	Quantitative semantics of the lambda calculus: Some generalisations of the relational model. LICS C.-H. Luke Ong
2016	A	`conf`	On Hierarchical Communication Topologies in the \pi -calculus. ESOP Emanuele D'Osualdo, C.-H. Luke Ong
2016	J	`jnl`	On Hierarchical Communication Topologies in the pi-calculus. CoRR Emanuele D'Osualdo, C.-H. Luke Ong
2016	A*	`conf`	Plays as Resource Terms via Non-idempotent Intersection Types. LICS Takeshi Tsukada, C.-H. Luke Ong
2016	A*	`conf`	Unboundedness and downward closures of higher-order pushdown automata. POPL Matthew Hague, Jonathan Kochems, C.-H. Luke Ong
2015	A	`conf`	Detecting redundant CSS rules in HTML5 applications: a tree rewriting approach. OOPSLA Matthew Hague, Anthony Widjaja Lin, C.-H. Luke Ong
2015	B	`conf`	Fragments of ML Decidable by Nested Data Class Memory Automata. FoSSaCS Conrad Cotton-Barratt, David Hopkins, Andrzej S. Murawski, C.-H. Luke Ong
2015	J	`jnl`	Fragments of ML Decidable by Nested Data Class Memory Automata. CoRR Conrad Cotton-Barratt, David Hopkins, Andrzej S. Murawski, C.-H. Luke Ong
2015	J	`jnl`	Logic, Language, Information and Computation (WoLLIC 2012). Theor. Comput. Sci. C.-H. Luke Ong, Ruy J. G. B. de Queiroz
2015	A*	`conf`	Nondeterminism in Game Semantics via Sheaves. LICS Takeshi Tsukada, C.-H. Luke Ong
2015	J	`jnl`	Normalisation by Traversals. CoRR C.-H. Luke Ong
2015	J	`jnl`	Unboundedness and Downwards Closures of Higher-Order Pushdown Automata. CoRR Matthew Hague, Jonathan Kochems, C.-H. Luke Ong
2015	C	`conf`	Weak and Nested Class Memory Automata. LATA Conrad Cotton-Barratt, Andrzej S. Murawski, C.-H. Luke Ong
2014	A*	`conf`	A type-directed abstraction refinement approach to higher-order model checking. POPL Steven J. Ramsay, Robin P. Neatherway, C.-H. Luke Ong
2014	—	`conf`	Compositional higher-order model checking via CSL-LICS Takeshi Tsukada, C.-H. Luke Ong
2014	J	`jnl`	Decidable Models of Recursive Asynchronous Concurrency. CoRR Jonathan Kochems, C.-H. Luke Ong
2014	J	`jnl`	Innocent Strategies are Sheaves over Plays - Deterministic, Non-deterministic and Probabilistic Innocence. CoRR Takeshi Tsukada, C.-H. Luke Ong
2014	J	`jnl`	Safety verification of asynchronous pushdown systems with shaped stacks. CoRR Jonathan Kochems, C.-H. Luke Ong
2014	—	`conf`	TravMC2: higher-order model checking for alternating parity tree automata. SPIN Robin P. Neatherway, C.-H. Luke Ong
2014	J	`jnl`	Weak and Nested Class Memory Automata. CoRR Conrad Cotton-Barratt, Andrzej S. Murawski, C.-H. Luke Ong
2013	J	`jnl`	Automatic Verification of Erlang-Style Concurrency CoRR Emanuele D'Osualdo, Jonathan Kochems, C.-H. Luke Ong
2013	B	`conf`	Automatic Verification of Erlang-Style Concurrency. SAS Emanuele D'Osualdo, Jonathan Kochems, C.-H. Luke Ong
2013	J	`jnl`	Information Flow Analysis for a Dynamically Typed Functional Language with Staged Metaprogramming CoRR Martin Lester, C.-H. Luke Ong, Max Schäfer
2013	B	`conf`	Safety Verification of Asynchronous Pushdown Systems with Shaped Stacks. CONCUR Jonathan Kochems, C.-H. Luke Ong
2012	A	`conf`	A traversal-based algorithm for higher-order model checking. ICFP Robin P. Neatherway, Steven J. Ramsay, C.-H. Luke Ong
2012	A*	`conf`	Hector: An Equivalence Checker for a Higher-Order Fragment of ML. CAV David Hopkins, Andrzej S. Murawski, C.-H. Luke Ong
2012	C	`ed.`	Logic, Language, Information and Computation - 19th International Workshop, WoLLIC 2012, Buenos Aires, Argentina, September 3-6, 2012. Proceedings WoLLIC C.-H. Luke Ong, Ruy J. G. B. de Queiroz
2012	—	`conf`	Two-Level Game Semantics, Intersection Types, and Recursion Schemes. ICALP (2) C.-H. Luke Ong, Takeshi Tsukada
2011	Misc	`ed.`	5th IEEE International Symposium on Theoretical Aspects of Software Engineering, TASE 2011, Xi'an, China, 29-31 August 2011 TASE Zhenhua Duan, C.-H. Luke Ong
2011	—	`conf`	A Fragment of ML Decidable by Visibly Pushdown Automata. ICALP (2) David Hopkins, Andrzej S. Murawski, C.-H. Luke Ong
2011	J	`jnl`	A saturation method for the modal μ-calculus over pushdown systems. Inf. Comput. Matthew Hague, C.-H. Luke Ong
2011	J	`jnl`	Complexity of Model Checking Recursion Schemes for Fragments of the Modal Mu-Calculus Log. Methods Comput. Sci. Naoki Kobayashi, C.-H. Luke Ong
2011	—	`conf`	Improved Functional Flow and Reachability Analyses Using Indexed Linear Tree Grammars. RTA Jonathan Kochems, C.-H. Luke Ong
2011	—	`ed.`	Typed Lambda Calculi and Applications - 10th International Conference, TLCA 2011, Novi Sad, Serbia, June 1-3, 2011. Proceedings TLCA C.-H. Luke Ong
2011	A*	`conf`	Verifying higher-order functional programs with pattern-matching algebraic data types. POPL C.-H. Luke Ong, Steven J. Ramsay
2010	J	`jnl`	A Saturation Method for the Modal Mu-Calculus with Backwards Modalities over Pushdown Systems CoRR Matthew Hague, C.-H. Luke Ong
2010	—	`conf`	Analysing Mu-Calculus Properties of Pushdown Systems. SPIN Matthew Hague, C.-H. Luke Ong
2010	A	`conf`	Boom: Taking Boolean Program Model Checking One Step Further. TACAS Gérard Basler, Matthew Hague, Daniel Kroening, C.-H. Luke Ong, Thomas Wahl, Haoxian Zhao
2010	B	`ed.`	Foundations of Software Science and Computational Structures, 13th International Conference, FOSSACS 2010, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2010, Paphos, Cyprus, March 20-28, 2010. Proceedings FoSSaCS C.-H. Luke Ong
2010	—	`ch.`	Models of Higher-Order Computation: Recursion Schemes and Collapsible Pushdown Automata. Logics and Languages for Reliability and Security C.-H. Luke Ong
2010	A*	`conf`	Recursion Schemes and Logical Reflection. LICS Christopher H. Broadbent, Arnaud Carayol, C.-H. Luke Ong, Olivier Serre
2009	A*	`conf`	A Type System Equivalent to the Modal Mu-Calculus Model Checking of Higher-Order Recursion Schemes. LICS Naoki Kobayashi, C.-H. Luke Ong
2009	—	`conf`	Complexity of Model Checking Recursion Schemes for Fragments of the Modal Mu-Calculus. ICALP (2) Naoki Kobayashi, C.-H. Luke Ong
2009	A*	`conf`	Functional Reachability. LICS C.-H. Luke Ong, Nikos Tzevelekos
2009	A*	`conf`	Homer: A Higher-Order Observational Equivalence Model checkER. CAV David Hopkins, C.-H. Luke Ong
2009	B	`conf`	On Global Model Checking Trees Generated by Higher-Order Recursion Schemes. FoSSaCS Christopher H. Broadbent, C.-H. Luke Ong
2009	J	`jnl`	The Safe Lambda Calculus Log. Methods Comput. Sci. William Blum, C.-H. Luke Ong
2009	B	`conf`	Winning Regions of Pushdown Parity Games: A Saturation Method. CONCUR Matthew Hague, C.-H. Luke Ong
2008	A*	`conf`	Collapsible Pushdown Automata and Recursion Schemes. LICS Matthew Hague, Andrzej S. Murawski, C.-H. Luke Ong, Olivier Serre
2008	—	`ed.`	Fifth IFIP International Conference On Theoretical Computer Science - TCS 2008, IFIP 20th World Computer Congress, TC 1, Foundations of Computer Science, September 7-10, 2008, Milano, Italy IFIP TCS Giorgio Ausiello, Juhani Karhumäki, Giancarlo Mauri, C.-H. Luke Ong
2008	J	`jnl`	Symbolic Backwards-Reachability Analysis for Higher-Order Pushdown Systems CoRR Matthew Hague, C.-H. Luke Ong
2008	J	`jnl`	Symbolic Backwards-Reachability Analysis for Higher-Order Pushdown Systems. Log. Methods Comput. Sci. Matthew Hague, C.-H. Luke Ong
2008	A	`conf`	Verification of Higher-Order Computation: A Game-Semantic Approach. ESOP C.-H. Luke Ong
2008	A*	`conf`	Winning Regions of Higher-Order Pushdown Games. LICS Arnaud Carayol, Matthew Hague, Antoine Meyer, C.-H. Luke Ong, Olivier Serre
2007	—	`conf`	Fully abstract semantics of additive aspects by translation. AOSD Sam Bakhtiar Sanjabi, C.-H. Luke Ong
2007	B	`conf`	Hierarchies of Infinite Structures Generated by Pushdown Automata and Recursion Schemes. MFCS C.-H. Luke Ong
2007	B	`conf`	Symbolic Backwards-Reachability Analysis for Higher-Order Pushdown Systems. FoSSaCS Matthew Hague, C.-H. Luke Ong
2007	—	`conf`	The Safe Lambda Calculus. TLCA William Blum, C.-H. Luke Ong
2006	J	`jnl`	Fast verification of MLL proof nets via IMLL. ACM Trans. Comput. Log. Andrzej S. Murawski, C.-H. Luke Ong
2006	A*	`conf`	On Model-Checking Trees Generated by Higher-Order Recursion Schemes. LICS C.-H. Luke Ong
2006	B	`conf`	Some Results on a Game-Semantic Approach to Verifying Finitely-Presentable Infinite Structures (Extended Abstract). CSL C.-H. Luke Ong
2006	J	`jnl`	Syntactic control of concurrency. Theor. Comput. Sci. Dan R. Ghica, Andrzej S. Murawski, C.-H. Luke Ong
2005	B	`ed.`	Computer Science Logic, 19th International Workshop, CSL 2005, 14th Annual Conference of the EACSL, Oxford, UK, August 22-25, 2005, Proceedings CSL C.-H. Luke Ong
2005	A*	`conf`	Idealized Algol with Ground Recursion, and DPDA Equivalence. ICALP Andrzej S. Murawski, C.-H. Luke Ong, Igor Walukiewicz
2005	B	`conf`	Safety Is not a Restriction at Level 2 for String Languages. FoSSaCS Klaus Aehlig, Jolie G. de Miranda, C.-H. Luke Ong
2005	—	`conf`	The Monadic Second Order Theory of Trees Given by Arbitrary Level-Two Recursion Schemes Is Decidable. TLCA Klaus Aehlig, Jolie G. de Miranda, C.-H. Luke Ong
2004	J	`jnl`	An approach to deciding the observational equivalence of Algol-like languages. Ann. Pure Appl. Log. C.-H. Luke Ong
2004	A	`conf`	Applying Game Semantics to Compositional Software Modeling and Verification. TACAS Samson Abramsky, Dan R. Ghica, Andrzej S. Murawski, C.-H. Luke Ong
2004	J	`jnl`	Games characterizing Levy-Longo trees. Theor. Comput. Sci. C.-H. Luke Ong, Pietro Di Gianantonio
2004	A*	`conf`	Nominal Games and Full Abstraction for the Nu-Calculus. LICS Samson Abramsky, Dan R. Ghica, Andrzej S. Murawski, C.-H. Luke Ong, Ian David Bede Stark
2004	J	`jnl`	On an interpretation of safe recursion in light affine logic. Theor. Comput. Sci. Andrzej S. Murawski, C.-H. Luke Ong
2004	A*	`conf`	Syntactic Control of Concurrency. ICALP Dan R. Ghica, Andrzej S. Murawski, C.-H. Luke Ong
2003	J	`jnl`	Adapting innocent game models for the Böhm treelambda -theory. Theor. Comput. Sci. Andrew D. Ker, Hanno Nickau, C.-H. Luke Ong
2003	J	`jnl`	Exhausting strategies, joker games and full completeness for IMLL with Unit. Theor. Comput. Sci. Andrzej S. Murawski, C.-H. Luke Ong
2002	A*	`conf`	Games Characterizing Levy-Longo Trees. ICALP C.-H. Luke Ong, Pietro Di Gianantonio
2002	J	`jnl`	Innocent game models of untyped lambda-calculus. Theor. Comput. Sci. Andrew D. Ker, Hanno Nickau, C.-H. Luke Ong
2002	—	`conf`	Model Checking Algol-Like Languages Using Game Semantics. FSTTCS C.-H. Luke Ong
2002	A*	`conf`	Observational Equivalence of 3rd-Order Idealized Algol is Decidable. LICS C.-H. Luke Ong
2001	—	`conf`	Evolving Games and Essential Nets for Affine Polymorphism. TLCA Andrzej S. Murawski, C.-H. Luke Ong
2000	B	`conf`	Discreet Games, Light Affine Logic and PTIME Computation. CSL Andrzej S. Murawski, C.-H. Luke Ong
2000	A*	`conf`	Dominator Trees and Fast Verification of Proof Nets. LICS Andrzej S. Murawski, C.-H. Luke Ong
2000	B	`conf`	Light Logic and Resource Bounded Computation. APLAS C.-H. Luke Ong
2000	J	`jnl`	On Full Abstraction for PCF: I, II, and III. Inf. Comput. J. M. E. Hyland, C.-H. Luke Ong
1999	B	`conf`	A Universal Innocent Game Model for the Böhm Tree Lambda Theory. CSL Andrew D. Ker, Hanno Nickau, C.-H. Luke Ong
1999	—	`conf`	Exhausting Strategies, Joker Games and IMLL with Units. CTCS Andrzej S. Murawski, C.-H. Luke Ong
1999	—	`conf`	Internal Languages for Autonomous and *-Autonomous Categories. CTCS Thong wei Koh, C.-H. Luke Ong
1997	A*	`conf`	A Curry-Howard Foundation for Functional Computation with Control. POPL C.-H. Luke Ong, Charles A. Stewart
1996	A*	`conf`	A Semantic View of Classical Proofs: Type-Theoretic, Categorical, and Denotational Characterizations (Preliminary Extended Abstract). LICS C.-H. Luke Ong
1995	—	`conf`	Pi-Calculus, Dialogue Games and PCF. FPCA J. M. E. Hyland, C.-H. Luke Ong
1993	B	`conf`	A Generic Strong Normalization Argument: Application to the Calculus of Constructions. CSL C.-H. Luke Ong, Eike Ritter
1993	J	`jnl`	Full Abstraction in the Lazy Lambda Calculus Inf. Comput. Samson Abramsky, C.-H. Luke Ong
1993	—	`conf`	Modified Realizability Toposes and Strong Normalization Proofs. TLCA J. M. E. Hyland, C.-H. Luke Ong
1993	A*	`conf`	Non-Determinism in a Functional Setting LICS C.-H. Luke Ong
1992	A*	`conf`	Lazy Lambda Calculus: Theories, Models and Local Structure Characterization (Extended Abstract). ICALP C.-H. Luke Ong
1988	A*	`conf`	Fully Abstract Models of the Lazy Lambda Calculus FOCS C.-H. Luke Ong