Stop the war!Остановите войну!
for scientists:
default search action
Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCIDC.-H. Luke Ong
Chih-Hao Luke Ong – Luke Ong
Person information
- affiliation: University of Oxford, UK
Refine list
refinements active!
zoomed in on ?? of ?? records
view refined list in
export refined list as
showing all ?? records
2020 – today
- 2023
[c93]Basim Khajwal, C.-H. Luke Ong
, Dominik Wagner:
Fast and Correct Gradient-Based Optimisation for Probabilistic Programming via Smoothing. ESOP 2023: 479-506- [i38]Basim Khajwal, C.-H. Luke Ong, Dominik Wagner:
Fast and Correct Gradient-Based Optimisation for Probabilistic Programming via Smoothing. CoRR abs/2301.03415 (2023) - 2022
- [c92]Carol Mak, Fabian Zaiser, Luke Ong:
Nonparametric Involutive Markov Chain Monte Carlo. ICML 2022: 14802-14859 - [c91]Guanyan Li, Andrzej S. Murawski, Luke Ong:
Probabilistic Verification Beyond Context-Freeness. LICS 2022: 33:1-33:13 - [c90]Tim Reichelt, Luke Ong, Thomas Rainforth:
Rethinking Variational Inference for Probabilistic Programs with Stochastic Support. NeurIPS 2022 - [c89]Eddie Jones, C.-H. Luke Ong, Steven J. Ramsay:
CycleQ: an efficient basis for cyclic equational reasoning. PLDI 2022: 395-409 - [c88]Raven Beutner, C.-H. Luke Ong, Fabian Zaiser:
Guaranteed bounds for posterior inference in universal probabilistic programming. PLDI 2022: 536-551 - [c87]Tim Reichelt, Adam Golinski, Luke Ong, Tom Rainforth:
Expectation programming: Adapting probabilistic programming systems to estimate expectations efficiently. UAI 2022: 1676-1685 - [i37]Raven Beutner, Luke Ong, Fabian Zaiser:
Guaranteed Bounds for Posterior Inference in Universal Probabilistic Programming. CoRR abs/2204.02948 (2022) - [i36]Carol Mak, Fabian Zaiser, Luke Ong:
Nonparametric Involutive Markov Chain Monte Carlo. CoRR abs/2211.01100 (2022) - 2021
- [j23]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): 12:1-12:37 (2021) - [j22]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): 16:1-16:51 (2021) - [c86]Carol Mak, C.-H. Luke Ong, Hugo Paquet, Dominik Wagner:
Densities of Almost Surely Terminating Probabilistic Programs are Differentiable Almost Everywhere. ESOP 2021: 432-461 - [c85]Carol Mak, Fabian Zaiser, Luke Ong:
Nonparametric Hamiltonian Monte Carlo. ICML 2021: 7336-7347 - [c84]Toby Cathcart Burn, Luke Ong, Steven J. Ramsay, Dominik Wagner:
Initial Limit Datalog: a New Extensible Class of Decidable Constrained Horn Clauses. LICS 2021: 1-13 - [c83]Andrew Kenyon-Roberts, C.-H. Luke Ong:
Supermartingales, Ranking Functions and Probabilistic Lambda Calculus. LICS 2021: 1-13 - [c82]Raven Beutner, Luke Ong:
On probabilistic termination of functional programs with continuous distributions. PLDI 2021: 1312-1326 - [c81]Fabian Zaiser, Luke Ong:
Abstract: The Extended Theory of Trees and Algebraic (Co)datatypes. SMT 2021: 65 - [i35]Andrew Kenyon-Roberts, Luke Ong:
Supermartingales, Ranking Functions and Probabilistic Lambda Calculus. CoRR abs/2102.11164 (2021) - [i34]Raven Beutner, Luke Ong:
On Probabilistic Termination of Functional Programs with Continuous Distributions. CoRR abs/2104.04990 (2021) - [i33]Toby Cathcart Burn, Luke Ong, Steven J. Ramsay, Dominik Wagner:
Initial Limit Datalog: a New Extensible Class of Decidable Constrained Horn Clauses. CoRR abs/2104.14175 (2021) - [i32]Tim Reichelt, Adam Golinski, Luke Ong, Tom Rainforth:
Expectation Programming. CoRR abs/2106.04953 (2021) - [i31]Carol Mak, Fabian Zaiser, Luke Ong:
Nonparametric Hamiltonian Monte Carlo. CoRR abs/2106.10238 (2021) - [i30]Eddie Jones, C.-H. Luke Ong, Steven J. Ramsay:
CycleQ: An Efficient Basis for Cyclic Equational Reasoning. CoRR abs/2111.12553 (2021) - 2020
- [c80]Mario Alvarez-Picallo, C.-H. Luke Ong:
The Difference λ-Calculus: A Language for Difference Categories. FSCD 2020: 32:1-32:21 - [c79]Fabian Zaiser, C.-H. Luke Ong:
The Extended Theory of Trees and Algebraic (Co)datatypes. VPT/HCVS@ETAPS 2020: 167-196 - [i29]Carol Mak, Luke Ong:
A Differential-form Pullback Programming Language for Higher-order Reverse-mode Automatic Differentiation. CoRR abs/2002.08241 (2020) - [i28]Carol Mak, C.-H. Luke Ong, Hugo Paquet, Dominik Wagner:
Densities of almost-surely terminating probabilistic programs are differentiable almost everywhere. CoRR abs/2004.03924 (2020) - [i27]Christopher H. Broadbent, Arnaud Carayol, Matthew Hague, Andrzej S. Murawski, C.-H. Luke Ong, Olivier Serre:
Collapsible Pushdown Parity Games. CoRR abs/2010.06361 (2020) - [i26]Christopher H. Broadbent, Arnaud Carayol, C.-H. Luke Ong, Olivier Serre:
Higher-Order Recursion Schemes and Collapsible Pushdown Automata: Logical Properties. CoRR abs/2010.06366 (2020) - [i25]Mario Alvarez-Picallo, C.-H. Luke Ong:
The Difference Lambda-Calculus: A Language for Difference Categories. CoRR abs/2011.14476 (2020) - [i24]Martin Lester, Robin P. Neatherway, C.-H. Luke Ong, Steven J. Ramsay:
Verifying Liveness Properties of ML Programs. CoRR abs/2012.13333 (2020)
2010 – 2019
- 2019
- [j21]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): 11:1-11:38 (2019) - [c78]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: 525-552 - [c77]Mario Alvarez-Picallo, C.-H. Luke Ong:
Change Actions: Models of Generalised Differentiation. FoSSaCS 2019: 45-61 - [c76]Rolf Morel, Andrew Cropper, C.-H. Luke Ong:
Typed Meta-interpretive Learning of Logic Programs. JELIA 2019: 198-213 - [c75]C.-H. Luke Ong, Dominik Wagner:
HoCHC: A Refutationally Complete and Semantically Invariant System of Higher-order Logic Modulo Theories. LICS 2019: 1-14 - [i23]Mario Alvarez-Picallo, C.-H. Luke Ong:
Change Actions: Models of Generalised Differentiation. CoRR abs/1902.05465 (2019) - [i22]C.-H. Luke Ong, Dominik Wagner:
HoCHC: a Refutationally-complete and Semantically-invariant System of Higher-order Logic Modulo Theories. CoRR abs/1902.10396 (2019) - [i21]Anne Schreuder, C.-H. Luke Ong:
Polynomial Probabilistic Invariants and the Optional Stopping Theorem. CoRR abs/1910.12634 (2019) - 2018
- [j20]Egor Ianovski, Luke Ong:
The complexity of decision problems about equilibria in two-player Boolean games. Artif. Intell. 261: 1-15 (2018) - [j19]Egor Ianovski, Luke Ong:
Simulating cardinal preferences in Boolean games: A proof technique. Inf. Comput. 261: 488-518 (2018) - [j18]Toby Cathcart Burn, C.-H. Luke Ong, Steven J. Ramsay:
Higher-order constrained horn clauses for verification. Proc. ACM Program. Lang. 2(POPL): 11:1-11:28 (2018) - [c74]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: 889-898 - [c73]Zhao Duan, Cong Tian, Zhenhua Duan, C.-H. Luke Ong:
InterpChecker: Reducing State Space via Interpolations - (Competition Contribution). TACAS (2) 2018: 432-436 - [i20]Long Pham, Steven J. Ramsay, C.-H. Luke Ong:
Defunctionalization of Higher-Order Constrained Horn Clauses. CoRR abs/1810.03598 (2018) - [i19]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 abs/1811.06069 (2018) - 2017
- [j17]Matthew Hague, Andrzej S. Murawski, C.-H. Luke Ong, Olivier Serre:
Collapsible Pushdown Automata and Recursion Schemes. ACM Trans. Comput. Log. 18(3): 25:1-25:42 (2017) - [c72]Emanuele D'Osualdo, Luke Ong, Alwen Tiu:
Deciding Secrecy of Security Protocols for an Unbounded Number of Sessions: The Case of Depth-Bounded Processes. CSF 2017: 464-480 - [c71]Conrad Cotton-Barratt, Andrzej S. Murawski, C.-H. Luke Ong:
ML and Extended Branching VASS. ESOP 2017: 314-340 - [c70]C.-H. Luke Ong:
Automata, Logic and Games for the λ-Calculus. ICLA 2017: 23-26 - [c69]Cong Tian, Zhao Duan, Zhenhua Duan, C.-H. Luke Ong:
More effective interpolations in software model checking. ASE 2017: 183-193 - [c68]C.-H. Luke Ong:
Quantitative semantics of the lambda calculus: Some generalisations of the relational model. LICS 2017: 1-12 - [c67]Takeshi Tsukada, Kazuyuki Asada, C.-H. Luke Ong:
Generalised species of rigid resource terms. LICS 2017: 1-12 - [e8]Zhenhua Duan, Luke Ong:
Formal Methods and Software Engineering - 19th International Conference on Formal Engineering Methods, ICFEM 2017, Xi'an, China, November 13-17, 2017, Proceedings. Lecture Notes in Computer Science 10610, Springer 2017, ISBN 978-3-319-68689-9 [contents] - [i18]Toby Cathcart Burn, C.-H. Luke Ong, Steven J. Ramsay:
Higher-Order Constrained Horn Clauses and Refinement Types. CoRR abs/1705.06216 (2017) - 2016
- [j16]Martin Mariusz Lester, Luke Ong, Max Schäfer:
Information flow analysis for a dynamically typed language with staged metaprogramming. J. Comput. Secur. 24(5): 541-582 (2016) - [c66]Emanuele D'Osualdo, C.-H. Luke Ong:
On Hierarchical Communication Topologies in the \pi -calculus. ESOP 2016: 149-175 - [c65]Takeshi Tsukada, C.-H. Luke Ong:
Plays as Resource Terms via Non-idempotent Intersection Types. LICS 2016: 237-246 - [c64]Matthew Hague, Jonathan Kochems, C.-H. Luke Ong:
Unboundedness and downward closures of higher-order pushdown automata. POPL 2016: 151-163 - [i17]Emanuele D'Osualdo, C.-H. Luke Ong:
On Hierarchical Communication Topologies in the pi-calculus. CoRR abs/1601.01725 (2016) - [i16]Naoki Kobayashi, Luke Ong, Igor Walukiewicz:
Higher-Order Model Checking (NII Shonan Meeting 2016-4). NII Shonan Meet. Rep. 2016 (2016) - 2015
- [j15]C.-H. Luke Ong, Ruy J. G. B. de Queiroz:
Logic, Language, Information and Computation (WoLLIC 2012). Theor. Comput. Sci. 603: 1-2 (2015) - [c63]Conrad Cotton-Barratt, David Hopkins, Andrzej S. Murawski, C.-H. Luke Ong:
Fragments of ML Decidable by Nested Data Class Memory Automata. FoSSaCS 2015: 249-263 - [c62]Conrad Cotton-Barratt, Andrzej S. Murawski, C.-H. Luke Ong:
Weak and Nested Class Memory Automata. LATA 2015: 188-199 - [c61]Luke Ong:
Higher-Order Model Checking: An Overview. LICS 2015: 1-15 - [c60]Takeshi Tsukada, C.-H. Luke Ong:
Nondeterminism in Game Semantics via Sheaves. LICS 2015: 220-231 - [c59]Matthew Hague, Anthony Widjaja Lin, C.-H. Luke Ong:
Detecting redundant CSS rules in HTML5 applications: a tree rewriting approach. OOPSLA 2015: 1-19 - [i15]Conrad Cotton-Barratt, David Hopkins, Andrzej S. Murawski, C.-H. Luke Ong:
Fragments of ML Decidable by Nested Data Class Memory Automata. CoRR abs/1501.04511 (2015) - [i14]Emanuele D'Osualdo, Luke Ong:
A Type System for proving Depth Boundedness in the pi-calculus. CoRR abs/1502.00944 (2015) - [i13]Matthew Hague, Jonathan Kochems, C.-H. Luke Ong:
Unboundedness and Downwards Closures of Higher-Order Pushdown Automata. CoRR abs/1507.03304 (2015) - [i12]C.-H. Luke Ong:
Normalisation by Traversals. CoRR abs/1511.02629 (2015) - 2014
- [c58]Takeshi Tsukada, C.-H. Luke Ong:
Compositional higher-order model checking via ω-regular games over Böhm trees. CSL-LICS 2014: 78:1-78:10 - [c57]Egor Ianovski, Luke Ong:
EGuaranteeNash for Boolean Games Is NEXP-Hard. KR 2014 - [c56]Steven J. Ramsay, Robin P. Neatherway, C.-H. Luke Ong:
A type-directed abstraction refinement approach to higher-order model checking. POPL 2014: 61-72 - [c55]Robin P. Neatherway, C.-H. Luke Ong:
TravMC2: higher-order model checking for alternating parity tree automata. SPIN 2014: 129-132 - [i11]Jonathan Kochems, C.-H. Luke Ong:
Safety verification of asynchronous pushdown systems with shaped stacks. CoRR abs/1401.6325 (2014) - [i10]Conrad Cotton-Barratt, Andrzej S. Murawski, C.-H. Luke Ong:
Weak and Nested Class Memory Automata. CoRR abs/1409.1136 (2014) - [i9]Takeshi Tsukada, C.-H. Luke Ong:
Innocent Strategies are Sheaves over Plays - Deterministic, Non-deterministic and Probabilistic Innocence. CoRR abs/1409.2764 (2014) - [i8]Jonathan Kochems, C.-H. Luke Ong:
Decidable Models of Recursive Asynchronous Concurrency. CoRR abs/1410.8852 (2014) - [i7]Matthew Hague, Anthony Widjaja Lin, Luke Ong:
Detecting Redundant CSS Rules in HTML5 Applications: A Tree-Rewriting Approach. CoRR abs/1412.5143 (2014) - 2013
- [c54]Jonathan Kochems, C.-H. Luke Ong:
Safety Verification of Asynchronous Pushdown Systems with Shaped Stacks. CONCUR 2013: 288-302 - [c53]Martin Lester, Luke Ong, Max Schäfer:
Information Flow Analysis for a Dynamically Typed Language with Staged Metaprogramming. CSF 2013: 209-223 - [c52]Luke Ong:
Recursion Schemes, Collapsible Pushdown Automata and Higher-Order Model Checking. LATA 2013: 13-41 - [c51]Emanuele D'Osualdo, Jonathan Kochems, C.-H. Luke Ong:
Automatic Verification of Erlang-Style Concurrency. SAS 2013: 454-476 - [e7]Bob Coecke, Luke Ong, Prakash Panangaden:
Computation, Logic, Games, and Quantum Foundations. The Many Facets of Samson Abramsky - Essays Dedicated to Samson Abramsky on the Occasion of His 60th Birthday. Lecture Notes in Computer Science 7860, Springer 2013, ISBN 978-3-642-38163-8 [contents] - [i6]Martin Lester, C.-H. Luke Ong, Max Schäfer:
Information Flow Analysis for a Dynamically Typed Functional Language with Staged Metaprogramming. CoRR abs/1302.3178 (2013) - [i5]Emanuele D'Osualdo, Jonathan Kochems, C.-H. Luke Ong:
Automatic Verification of Erlang-Style Concurrency. CoRR abs/1303.2201 (2013) - [i4]Egor Ianovski, Luke Ong:
EGuaranteeNash for Boolean Games is NEXP-Hard. CoRR abs/1312.4114 (2013) - 2012
- [c50]Emanuele D'Osualdo, Jonathan Kochems, Luke Ong:
Soter: an automatic safety verifier for erlang. AGERE!@SPLASH 2012: 137-140 - [c49]David Hopkins, Andrzej S. Murawski, C.-H. Luke Ong:
Hector: An Equivalence Checker for a Higher-Order Fragment of ML. CAV 2012: 774-780 - [c48]C.-H. Luke Ong, Takeshi Tsukada:
Two-Level Game Semantics, Intersection Types, and Recursion Schemes. ICALP (2) 2012: 325-336 - [c47]Robin P. Neatherway, Steven J. Ramsay, C.-H. Luke Ong:
A traversal-based algorithm for higher-order model checking. ICFP 2012: 353-364 - [e6]C.-H. Luke Ong, Ruy J. G. B. de Queiroz:
Logic, Language, Information and Computation - 19th International Workshop, WoLLIC 2012, Buenos Aires, Argentina, September 3-6, 2012. Proceedings. Lecture Notes in Computer Science 7456, Springer 2012, ISBN 978-3-642-32620-2 [contents] - 2011
- [j14]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) - [j13]Matthew Hague, C.-H. Luke Ong:
A saturation method for the modal μ-calculus over pushdown systems. Inf. Comput. 209(5): 799-821 (2011) - [c46]David Hopkins, Andrzej S. Murawski, C.-H. Luke Ong:
A Fragment of ML Decidable by Visibly Pushdown Automata. ICALP (2) 2011: 149-161 - [c45]C.-H. Luke Ong, Steven J. Ramsay:
Verifying higher-order functional programs with pattern-matching algebraic data types. POPL 2011: 587-598 - [c44]Jonathan Kochems, C.-H. Luke Ong:
Improved Functional Flow and Reachability Analyses Using Indexed Linear Tree Grammars. RTA 2011: 187-202 - [e5]Zhenhua Duan, C.-H. Luke Ong:
5th IEEE International Symposium on Theoretical Aspects of Software Engineering, TASE 2011, Xi'an, China, 29-31 August 2011. IEEE Computer Society 2011, ISBN 978-1-4577-1487-0 [contents] - [e4]C.-H. Luke Ong:
Typed Lambda Calculi and Applications - 10th International Conference, TLCA 2011, Novi Sad, Serbia, June 1-3, 2011. Proceedings. Lecture Notes in Computer Science 6690, Springer 2011, ISBN 978-3-642-21690-9 [contents] - [i3]Naoki Kobayashi, Luke Ong, David Van Horn:
Automated Techniques for Higher-Order Program Verification (NII Shonan Meeting 2011-5). NII Shonan Meet. Rep. 2011 (2011) - 2010
- [c43]Christopher H. Broadbent, Arnaud Carayol, C.-H. Luke Ong, Olivier Serre:
Recursion Schemes and Logical Reflection. LICS 2010: 120-129 - [c42]Matthew Hague, C.-H. Luke Ong:
Analysing Mu-Calculus Properties of Pushdown Systems. SPIN 2010: 187-192 - [c41]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: 145-149 - [p1]C.-H. Luke Ong:
Models of Higher-Order Computation: Recursion Schemes and Collapsible Pushdown Automata. Logics and Languages for Reliability and Security 2010: 263-299 - [e3]C.-H. Luke Ong:
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. Lecture Notes in Computer Science 6014, Springer 2010, ISBN 978-3-642-12031-2 [contents] - [i2]Matthew Hague, C.-H. Luke Ong:
A Saturation Method for the Modal Mu-Calculus with Backwards Modalities over Pushdown Systems. CoRR abs/1006.5906 (2010)
2000 – 2009
- 2009
- [j12]William Blum, C.-H. Luke Ong:
The Safe Lambda Calculus. Log. Methods Comput. Sci. 5(1) (2009) - [c40]David Hopkins, C.-H. Luke Ong:
Homer: A Higher-Order Observational Equivalence Model checkER. CAV 2009: 654-660 - [c39]Matthew Hague, C.-H. Luke Ong:
Winning Regions of Pushdown Parity Games: A Saturation Method. CONCUR 2009: 384-398 - [c38]Christopher H. Broadbent, C.-H. Luke Ong:
On Global Model Checking Trees Generated by Higher-Order Recursion Schemes. FoSSaCS 2009: 107-121 - [c37]Naoki Kobayashi, C.-H. Luke Ong:
Complexity of Model Checking Recursion Schemes for Fragments of the Modal Mu-Calculus. ICALP (2) 2009: 223-234 - [c36]Naoki Kobayashi, C.-H. Luke Ong:
A Type System Equivalent to the Modal Mu-Calculus Model Checking of Higher-Order Recursion Schemes. LICS 2009: 179-188 - [c35]C.-H. Luke Ong, Nikos Tzevelekos:
Functional Reachability. LICS 2009: 286-295 - 2008
- [j11]Matthew Hague, C.-H. Luke Ong:
Symbolic Backwards-Reachability Analysis for Higher-Order Pushdown Systems. Log. Methods Comput. Sci. 4(4) (2008) - [c34]C.-H. Luke Ong:
Verification of Higher-Order Computation: A Game-Semantic Approach. ESOP 2008: 299-306 - [c33]Arnaud Carayol, Matthew Hague, Antoine Meyer, C.-H. Luke Ong, Olivier Serre:
Winning Regions of Higher-Order Pushdown Games. LICS 2008: 193-204 - [c32]Matthew Hague, Andrzej S. Murawski, C.-H. Luke Ong, Olivier Serre:
Collapsible Pushdown Automata and Recursion Schemes. LICS 2008: 452-461 - [e2]Giorgio Ausiello, Juhani Karhumäki, Giancarlo Mauri, C.-H. Luke Ong:
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 273, Springer 2008, ISBN 978-0-387-09679-7 [contents] - [i1]Matthew Hague, C.-H. Luke Ong:
Symbolic Backwards-Reachability Analysis for Higher-Order Pushdown Systems. CoRR abs/0811.1103 (2008) - 2007
- [c31]S. B. Sanjabi, C.-H. Luke Ong