C.-H. Luke Ong

Orcid: 0000-0001-7509-680X

Affiliations:
  • University of Oxford, UK


According to our database1, C.-H. Luke Ong authored at least 134 papers between 1988 and 2024.

Collaborative distances:

Timeline

Legend:

Book 
In proceedings 
Article 
PhD thesis 
Dataset
Other 

Links

Online presence:

On csauthors.net:

Bibliography

2024
Static Posterior Inference of Bayesian Probabilistic Programming via Polynomial Solving.
Proc. ACM Program. Lang., 2024

Reinforcement Learning with LTL and ω-Regular Objectives via Optimality-Preserving Translation to Average Rewards.
CoRR, 2024

Towards Interpreting Visual Information Processing in Vision-Language Models.
CoRR, 2024

Unifying Qualitative and Quantitative Safety Verification of DNN-Controlled Systems.
Proceedings of the Computer Aided Verification - 36th International Conference, 2024

Diagonalisation SGD: Fast & Convergent SGD for Non-Differentiable Models via Reparameterisation and Smoothing.
Proceedings of the International Conference on Artificial Intelligence and Statistics, 2024

Beyond Bayesian Model Averaging over Paths in Probabilistic Programs with Stochastic Support.
Proceedings of the International Conference on Artificial Intelligence and Statistics, 2024

2023
Template-Based Static Posterior Inference for Bayesian Probabilistic Programming.
CoRR, 2023

Exact Bayesian Inference on Discrete Models via Probability Generating Functions: A Probabilistic Programming Approach.
Proceedings of the Advances in Neural Information Processing Systems 36: Annual Conference on Neural Information Processing Systems 2023, 2023

Fast and Correct Gradient-Based Optimisation for Probabilistic Programming via Smoothing.
Proceedings of the Programming Languages and Systems, 2023

2022
Expectation programming: Adapting probabilistic programming systems to estimate expectations efficiently.
Proceedings of the Uncertainty in Artificial Intelligence, 2022

CycleQ: an efficient basis for cyclic equational reasoning.
Proceedings of the PLDI '22: 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation, San Diego, CA, USA, June 13, 2022

Guaranteed bounds for posterior inference in universal probabilistic programming.
Proceedings of the PLDI '22: 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation, San Diego, CA, USA, June 13, 2022

Rethinking Variational Inference for Probabilistic Programs with Stochastic Support.
Proceedings of the Advances in Neural Information Processing Systems 35: Annual Conference on Neural Information Processing Systems 2022, 2022

Probabilistic Verification Beyond Context-Freeness.
Proceedings of the LICS '22: 37th Annual ACM/IEEE Symposium on Logic in Computer Science, Haifa, Israel, August 2, 2022

Nonparametric Involutive Markov Chain Monte Carlo.
Proceedings of the International Conference on Machine Learning, 2022

2021
Higher-order Recursion Schemes and Collapsible Pushdown Automata: Logical Properties.
ACM Trans. Comput. Log., 2021

Collapsible Pushdown Parity Games.
ACM Trans. Comput. Log., 2021

Expectation Programming.
CoRR, 2021

Abstract: The Extended Theory of Trees and Algebraic (Co)datatypes.
Proceedings of the 19th International Workshop on Satisfiability Modulo Theories co-located with 33rd International Conference on Computer Aided Verification(CAV 2021), 2021

On probabilistic termination of functional programs with continuous distributions.
Proceedings of the PLDI '21: 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation, 2021

Supermartingales, Ranking Functions and Probabilistic Lambda Calculus.
Proceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science, 2021

Initial Limit Datalog: a New Extensible Class of Decidable Constrained Horn Clauses.
Proceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science, 2021

Nonparametric Hamiltonian Monte Carlo.
Proceedings of the 38th International Conference on Machine Learning, 2021

Densities of Almost Surely Terminating Probabilistic Programs are Differentiable Almost Everywhere.
Proceedings of the Programming Languages and Systems, 2021

2020
Verifying Liveness Properties of ML Programs.
CoRR, 2020

The Difference Lambda-Calculus: A Language for Difference Categories.
CoRR, 2020

The Extended Theory of Trees and Algebraic (Co)datatypes.
Proceedings of the Proceedings 8th International Workshop on Verification and Program Transformation and 7th Workshop on Horn Clauses for Verification and Synthesis, 2020

A Differential-form Pullback Programming Language for Higher-order Reverse-mode Automatic Differentiation.
CoRR, 2020

The Difference λ-Calculus: A Language for Difference Categories.
Proceedings of the 5th International Conference on Formal Structures for Computation and Deduction, 2020

2019
ML, Visibly Pushdown Class Memory Automata, and Extended Branching Vector Addition Systems with States.
ACM Trans. Program. Lang. Syst., 2019

Polynomial Probabilistic Invariants and the Optional Stopping Theorem.
CoRR, 2019

HoCHC: A Refutationally Complete and Semantically Invariant System of Higher-order Logic Modulo Theories.
Proceedings of the 34th Annual ACM/IEEE Symposium on Logic in Computer Science, 2019

Typed Meta-interpretive Learning of Logic Programs.
Proceedings of the Logics in Artificial Intelligence - 16th European Conference, 2019

Change Actions: Models of Generalised Differentiation.
Proceedings of the Foundations of Software Science and Computation Structures, 2019

Fixing Incremental Computation - Derivatives of Fixpoints, and the Recursive Semantics of Datalog.
Proceedings of the Programming Languages and Systems, 2019

2018
Higher-order constrained horn clauses for verification.
Proc. ACM Program. Lang., 2018

Simulating cardinal preferences in Boolean games: A proof technique.
Inf. Comput., 2018

Defunctionalization of Higher-Order Constrained Horn Clauses.
CoRR, 2018

The complexity of decision problems about equilibria in two-player Boolean games.
Artif. Intell., 2018

InterpChecker: Reducing State Space via Interpolations - (Competition Contribution).
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2018

Species, Profunctors and Taylor Expansion Weighted by SMCC: A Unified Framework for Modelling Nondeterministic, Probabilistic and Quantum Programs.
Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, 2018

2017
Collapsible Pushdown Automata and Recursion Schemes.
ACM Trans. Comput. Log., 2017

Higher-Order Constrained Horn Clauses and Refinement Types.
CoRR, 2017

Generalised species of rigid resource terms.
Proceedings of the 32nd Annual ACM/IEEE Symposium on Logic in Computer Science, 2017

Quantitative semantics of the lambda calculus: Some generalisations of the relational model.
Proceedings of the 32nd Annual ACM/IEEE Symposium on Logic in Computer Science, 2017

More effective interpolations in software model checking.
Proceedings of the 32nd IEEE/ACM International Conference on Automated Software Engineering, 2017

Automata, Logic and Games for the λ-Calculus.
Proceedings of the Logic and Its Applications - 7th Indian Conference, 2017

ML and Extended Branching VASS.
Proceedings of the Programming Languages and Systems, 2017

Deciding Secrecy of Security Protocols for an Unbounded Number of Sessions: The Case of Depth-Bounded Processes.
Proceedings of the 30th IEEE Computer Security Foundations Symposium, 2017

2016
Higher-Order Model Checking (NII Shonan Meeting 2016-4).
NII Shonan Meet. Rep., 2016

Information flow analysis for a dynamically typed language with staged metaprogramming.
J. Comput. Secur., 2016

Unboundedness and downward closures of higher-order pushdown automata.
Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2016

Plays as Resource Terms via Non-idempotent Intersection Types.
Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, 2016

On Hierarchical Communication Topologies in the \pi -calculus.
Proceedings of the Programming Languages and Systems, 2016

2015
Logic, Language, Information and Computation (WoLLIC 2012).
Theor. Comput. Sci., 2015

Normalisation by Traversals.
CoRR, 2015

Unboundedness and Downwards Closures of Higher-Order Pushdown Automata.
CoRR, 2015

A Type System for proving Depth Boundedness in the pi-calculus.
CoRR, 2015

Detecting redundant CSS rules in HTML5 applications: a tree rewriting approach.
Proceedings of the 2015 ACM SIGPLAN International Conference on Object-Oriented Programming, 2015

Nondeterminism in Game Semantics via Sheaves.
Proceedings of the 30th Annual ACM/IEEE Symposium on Logic in Computer Science, 2015

Higher-Order Model Checking: An Overview.
Proceedings of the 30th Annual ACM/IEEE Symposium on Logic in Computer Science, 2015

Weak and Nested Class Memory Automata.
Proceedings of the Language and Automata Theory and Applications, 2015

Fragments of ML Decidable by Nested Data Class Memory Automata.
Proceedings of the Foundations of Software Science and Computation Structures, 2015

2014
Innocent Strategies are Sheaves over Plays - Deterministic, Non-deterministic and Probabilistic Innocence.
CoRR, 2014

Decidable Models of Recursive Asynchronous Concurrency.
CoRR, 2014

TravMC2: higher-order model checking for alternating parity tree automata.
Proceedings of the 2014 International Symposium on Model Checking of Software, 2014

A type-directed abstraction refinement approach to higher-order model checking.
Proceedings of the 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2014

EGuaranteeNash for Boolean Games Is NEXP-Hard.
Proceedings of the Principles of Knowledge Representation and Reasoning: Proceedings of the Fourteenth International Conference, 2014

Compositional higher-order model checking via <i>ω</i>-regular games over Böhm trees.
Proceedings of the Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), 2014

2013
Information Flow Analysis for a Dynamically Typed Functional Language with Staged Metaprogramming
CoRR, 2013

Automatic Verification of Erlang-Style Concurrency.
Proceedings of the Static Analysis - 20th International Symposium, 2013

Recursion Schemes, Collapsible Pushdown Automata and Higher-Order Model Checking.
Proceedings of the Language and Automata Theory and Applications, 2013

Safety Verification of Asynchronous Pushdown Systems with Shaped Stacks.
Proceedings of the CONCUR 2013 - Concurrency Theory - 24th International Conference, 2013

2012
A traversal-based algorithm for higher-order model checking.
Proceedings of the ACM SIGPLAN International Conference on Functional Programming, 2012

Two-Level Game Semantics, Intersection Types, and Recursion Schemes.
Proceedings of the Automata, Languages, and Programming - 39th International Colloquium, 2012

Hector: An Equivalence Checker for a Higher-Order Fragment of ML.
Proceedings of the Computer Aided Verification - 24th International Conference, 2012

Soter: an automatic safety verifier for erlang.
Proceedings of the 2nd edition on Programming systems, 2012

2011
Automated Techniques for Higher-Order Program Verification (NII Shonan Meeting 2011-5).
NII Shonan Meet. Rep., 2011

A saturation method for the modal μ-calculus over pushdown systems.
Inf. Comput., 2011

Complexity of Model Checking Recursion Schemes for Fragments of the Modal Mu-Calculus
Log. Methods Comput. Sci., 2011

Improved Functional Flow and Reachability Analyses Using Indexed Linear Tree Grammars.
Proceedings of the 22nd International Conference on Rewriting Techniques and Applications, 2011

Verifying higher-order functional programs with pattern-matching algebraic data types.
Proceedings of the 38th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2011

A Fragment of ML Decidable by Visibly Pushdown Automata.
Proceedings of the Automata, Languages and Programming - 38th International Colloquium, 2011

2010
Models of Higher-Order Computation: Recursion Schemes and Collapsible Pushdown Automata.
Proceedings of the Logics and Languages for Reliability and Security, 2010

A Saturation Method for the Modal Mu-Calculus with Backwards Modalities over Pushdown Systems
CoRR, 2010

Boom: Taking Boolean Program Model Checking One Step Further.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2010

Analysing Mu-Calculus Properties of Pushdown Systems.
Proceedings of the Model Checking Software, 2010

Recursion Schemes and Logical Reflection.
Proceedings of the 25th Annual IEEE Symposium on Logic in Computer Science, 2010

2009
The Safe Lambda Calculus
Log. Methods Comput. Sci., 2009

Functional Reachability.
Proceedings of the 24th Annual IEEE Symposium on Logic in Computer Science, 2009

A Type System Equivalent to the Modal Mu-Calculus Model Checking of Higher-Order Recursion Schemes.
Proceedings of the 24th Annual IEEE Symposium on Logic in Computer Science, 2009

On Global Model Checking Trees Generated by Higher-Order Recursion Schemes.
Proceedings of the Foundations of Software Science and Computational Structures, 2009

Winning Regions of Pushdown Parity Games: A Saturation Method.
Proceedings of the CONCUR 2009 - Concurrency Theory, 20th International Conference, 2009

Homer: A Higher-Order Observational Equivalence Model checkER.
Proceedings of the Computer Aided Verification, 21st International Conference, 2009

2008
Symbolic Backwards-Reachability Analysis for Higher-Order Pushdown Systems.
Log. Methods Comput. Sci., 2008

Winning Regions of Higher-Order Pushdown Games.
Proceedings of the Twenty-Third Annual IEEE Symposium on Logic in Computer Science, 2008

Verification of Higher-Order Computation: A Game-Semantic Approach.
Proceedings of the Programming Languages and Systems, 2008

2007
Hierarchies of Infinite Structures Generated by Pushdown Automata and Recursion Schemes.
Proceedings of the Mathematical Foundations of Computer Science 2007, 2007

Fully abstract semantics of additive aspects by translation.
Proceedings of the 6th International Conference on Aspect-Oriented Software Development, 2007

2006
Fast verification of MLL proof nets via IMLL.
ACM Trans. Comput. Log., 2006

Syntactic control of concurrency.
Theor. Comput. Sci., 2006

On Model-Checking Trees Generated by Higher-Order Recursion Schemes.
Proceedings of the 21th IEEE Symposium on Logic in Computer Science (LICS 2006), 2006

Some Results on a Game-Semantic Approach to Verifying Finitely-Presentable Infinite Structures (Extended Abstract).
Proceedings of the Computer Science Logic, 20th International Workshop, 2006

2005
The Monadic Second Order Theory of Trees Given by Arbitrary Level-Two Recursion Schemes Is Decidable.
Proceedings of the Typed Lambda Calculi and Applications, 7th International Conference, 2005

Idealized Algol with Ground Recursion, and DPDA Equivalence.
Proceedings of the Automata, Languages and Programming, 32nd International Colloquium, 2005

Safety Is not a Restriction at Level 2 for String Languages.
Proceedings of the Foundations of Software Science and Computational Structures, 2005

2004
Games characterizing Levy-Longo trees.
Theor. Comput. Sci., 2004

On an interpretation of safe recursion in light affine logic.
Theor. Comput. Sci., 2004

An approach to deciding the observational equivalence of Algol-like languages.
Ann. Pure Appl. Log., 2004

Applying Game Semantics to Compositional Software Modeling and Verification.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2004

Nominal Games and Full Abstraction for the Nu-Calculus.
Proceedings of the 19th IEEE Symposium on Logic in Computer Science (LICS 2004), 2004

2003
Exhausting strategies, joker games and full completeness for IMLL with Unit.
Theor. Comput. Sci., 2003

Adapting innocent game models for the Böhm treelambda -theory.
Theor. Comput. Sci., 2003

2002
Innocent game models of untyped lambda-calculus.
Theor. Comput. Sci., 2002

Route oscillations in I-BGP with route reflection.
Proceedings of the ACM SIGCOMM 2002 Conference on Applications, 2002

Observational Equivalence of 3rd-Order Idealized Algol is Decidable.
Proceedings of the 17th IEEE Symposium on Logic in Computer Science (LICS 2002), 2002

Model Checking Algol-Like Languages Using Game Semantics.
Proceedings of the FST TCS 2002: Foundations of Software Technology and Theoretical Computer Science, 2002

2001
Evolving Games and Essential Nets for Affine Polymorphism.
Proceedings of the Typed Lambda Calculi and Applications, 5th International Conference, 2001

2000
On Full Abstraction for PCF: I, II, and III.
Inf. Comput., 2000

Dominator Trees and Fast Verification of Proof Nets.
Proceedings of the 15th Annual IEEE Symposium on Logic in Computer Science, 2000

Discreet Games, Light Affine Logic and PTIME Computation.
Proceedings of the Computer Science Logic, 2000

Light Logic and Resource Bounded Computation.
Proceedings of the First Asian Workshop on Programming Languages and Systems, 2000

1999
Exhausting Strategies, Joker Games and IMLL with Units.
Proceedings of the Conference on Category Theory and Computer Science, 1999

Internal Languages for Autonomous and *-Autonomous Categories.
Proceedings of the Conference on Category Theory and Computer Science, 1999

A Universal Innocent Game Model for the Böhm Tree Lambda Theory.
Proceedings of the Computer Science Logic, 13th International Workshop, 1999

1997
A Curry-Howard Foundation for Functional Computation with Control.
Proceedings of the Conference Record of POPL'97: The 24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 1997

1996
A Semantic View of Classical Proofs: Type-Theoretic, Categorical, and Denotational Characterizations (Preliminary Extended Abstract).
Proceedings of the Proceedings, 1996

1995
Pi-Calculus, Dialogue Games and PCF.
Proceedings of the seventh international conference on Functional programming languages and computer architecture, 1995

1993
Full Abstraction in the Lazy Lambda Calculus
Inf. Comput., August, 1993

Modified Realizability Toposes and Strong Normalization Proofs.
Proceedings of the Typed Lambda Calculi and Applications, 1993

Non-Determinism in a Functional Setting
Proceedings of the Eighth Annual Symposium on Logic in Computer Science (LICS '93), 1993

A Generic Strong Normalization Argument: Application to the Calculus of Constructions.
Proceedings of the Computer Science Logic, 7th Workshop, 1993

1992
Lazy Lambda Calculus: Theories, Models and Local Structure Characterization (Extended Abstract).
Proceedings of the Automata, Languages and Programming, 19th International Colloquium, 1992

1988
Fully Abstract Models of the Lazy Lambda Calculus
Proceedings of the 29th Annual Symposium on Foundations of Computer Science, 1988


  Loading...