Person: C.-H. Luke Ong

DBLP: Ong:C==H=_Luke

Facilitated 3 volumes:

Ed

Ed

Ed

Contributed to:

2015

2015

2015

2015

2014

2014

2013

2012

2012

2012

2011

2011

2011

2010

2010

2009

2009

2009

2009

2008

2008

2007

2007

2006

2006

2005

2005

2005

2004

2004

2004

2002

2002

2001

2000

2000

1999

1997

1996

1995

1993

1993

1992

2017

2016

2017

2019

2016

2018

Wrote 51 papers:

FoSSaCS-2015-Cotton-BarrattH #automaton #decidability #memory management #ml

Fragments of ML Decidable by Nested Data Class Memory Automata (CCB, DH, ASM, CHLO), pp. 249–263.

LATA-2015-Cotton-BarrattMO #automaton #memory management

Weak and Nested Class Memory Automata (CCB, ASM, CHLO), pp. 188–199.

LICS-2015-TsukadaO #game studies #nondeterminism #semantics

Nondeterminism in Game Semantics via Sheaves (TT, CHLO), pp. 220–231.

OOPSLA-2015-HagueLO #approach #css #detection #html

Detecting redundant CSS rules in HTML5 applications: a tree rewriting approach (MH, AWL, CHLO), pp. 1–19.

LICS-CSL-2014-TsukadaO #composition #game studies #higher-order #model checking

Compositional higher-order model checking via ω-regular games over Böhm trees (TT, CHLO), p. 10.

POPL-2014-RamsayNO #abstraction #approach #higher-order #model checking #refinement

A type-directed abstraction refinement approach to higher-order model checking (SJR, RPN, CHLO), pp. 61–72.

SAS-2013-DOsualdoKO #automation #concurrent #verification

Automatic Verification of Erlang-Style Concurrency (ED, JK, CHLO), pp. 454–476.

CAV-2012-HopkinsMO #equivalence #higher-order #ml #named

Hector: An Equivalence Checker for a Higher-Order Fragment of ML (DH, ASM, CHLO), pp. 774–780.

ICALP-v2-2012-OngT #game studies #recursion #semantics

Two-Level Game Semantics, Intersection Types, and Recursion Schemes (CHLO, TT), pp. 325–336.

ICFP-2012-NeatherwayRO #algorithm #higher-order #model checking

A traversal-based algorithm for higher-order model checking (RPN, SJR, CHLO), pp. 353–364.

ICALP-v2-2011-HopkinsMO #automaton #decidability #ml

A Fragment of ML Decidable by Visibly Pushdown Automata (DH, ASM, CHLO), pp. 149–161.

POPL-2011-OngR #algebra #data type #functional #higher-order #pattern matching #source code #verification

Verifying higher-order functional programs with pattern-matching algebraic data types (CHLO, SJR), pp. 587–598.

RTA-2011-KochemsO #analysis #functional #linear #reachability #using

Improved Functional Flow and Reachability Analyses Using Indexed Linear Tree Grammars (JK, CHLO), pp. 187–202.

LICS-2010-BroadbentCOS #logic #recursion

Recursion Schemes and Logical Reflection (CHB, AC, CHLO, OS), pp. 120–129.

TACAS-2010-BaslerHKOWZ #model checking #named

Boom: Taking Boolean Program Model Checking One Step Further (GB, MH, DK, CHLO, TW, HZ), pp. 145–149.

CAV-2009-HopkinsO #equivalence #higher-order #model checking #named

Homer: A Higher-Order Observational Equivalence Model checkER (DH, CHLO), pp. 654–660.

FoSSaCS-2009-BroadbentO #higher-order #model checking #on the #recursion

On Global Model Checking Trees Generated by Higher-Order Recursion Schemes (CHB, CHLO), pp. 107–121.

ICALP-v2-2009-KobayashiO #calculus #complexity #model checking #recursion #μ-calculus

Complexity of Model Checking Recursion Schemes for Fragments of the Modal μ-Calculus (NK, CHLO), pp. 223–234.

LICS-2009-KobayashiO #calculus #higher-order #model checking #recursion #type system #μ-calculus

A Type System Equivalent to the Modal μ-Calculus Model Checking of Higher-Order Recursion Schemes (NK, CHLO), pp. 179–188.

LICS-2009-OngT #functional #reachability

Functional Reachability (CHLO, NT), pp. 286–295.

ESOP-2008-Ong #approach #higher-order #semantics #verification

Verification of Higher-Order Computation: A Game-Semantic Approach (CHLO), pp. 299–306.

LICS-2008-CarayolHMOS #automaton #game studies #higher-order

Winning Regions of Higher-Order Pushdown Games (AC, MH, AM, CHLO, OS), pp. 193–204.

LICS-2008-HagueMOS #automaton #recursion

Collapsible Pushdown Automata and Recursion Schemes (MH, ASM, CHLO, OS), pp. 452–461.

FoSSaCS-2007-HagueO #analysis #automaton #higher-order

Symbolic Backwards-Reachability Analysis for Higher-Order Pushdown Systems (MH, CHLO), pp. 213–227.

TLCA-2007-BlumO #λ-calculus

The Safe λ Calculus (WB, CHLO), pp. 39–53.

CSL-2006-Ong #approach #infinity #semantics #verification

Some Results on a Game-Semantic Approach to Verifying Finitely-Presentable Infinite Structures (CHLO), pp. 31–40.

LICS-2006-Ong #higher-order #model checking #on the #recursion

On Model-Checking Trees Generated by Higher-Order Recursion Schemes (CHLO), pp. 81–90.

FoSSaCS-2005-AehligMO #safety #strict #string

Safety Is not a Restriction at Level 2 for String Languages (KA, JGdM, CHLO), pp. 490–504.

ICALP-2005-MurawskiOW #algol #equivalence #recursion

Idealized Algol with Ground Recursion, and DPDA Equivalence (ASM, CHLO, IW), pp. 917–929.

TLCA-2005-AehligMO #decidability #higher-order #monad #recursion

The Monadic Second Order Theory of Trees Given by Arbitrary Level-Two Recursion Schemes Is Decidable (KA, JGdM, CHLO), pp. 39–54.

ICALP-2004-GhicaMO #concurrent

Syntactic Control of Concurrency (DRG, ASM, CHLO), pp. 683–694.

LICS-2004-AbramskyGMOS #abstraction #calculus #game studies

Nominal Games and Full Abstraction for the Nu-Calculus (SA, DRG, ASM, CHLO, IDBS), pp. 150–159.

TACAS-2004-AbramskyGMO #composition #game studies #modelling #semantics #verification

Applying Game Semantics to Compositional Software Modeling and Verification (SA, DRG, ASM, CHLO), pp. 421–435.

ICALP-2002-OngG #game studies

Games Characterizing Levy-Longo Trees (CHLO, PDG), pp. 476–487.

LICS-2002-Ong #algol #decidability #equivalence

Observational Equivalence of 3rd-Order Idealized Algol is Decidable (CHLO), pp. 245–256.

TLCA-2001-MurawskiO #evolution #game studies #morphism #polymorphism

Evolving Games and Essential Nets for Affine Polymorphism (ASM, CHLO), pp. 360–375.

CSL-2000-MurawskiO #game studies #logic

Discreet Games, Light Affine Logic and PTIME Computation (ASM, CHLO), pp. 427–441.

LICS-2000-MurawskiO #performance #proving #verification

Dominator Trees and Fast Verification of Proof Nets (ASM, CHLO), pp. 181–191.

CSL-1999-KerNO #game studies

A Universal Innocent Game Model for the Böhm Tree λ Theory (ADK, HN, CHLO), pp. 405–419.

POPL-1997-OngS #functional

A Curry-Howard Foundation for Functional Computation with Control (CHLO, CAS), pp. 215–227.

LICS-1996-Ong #category theory #proving #semantics

A Semantic View of Classical Proofs: Type-Theoretic, Categorical, and Denotational Characterizations (CHLO), pp. 230–241.

FPCA-1995-HylandO #game studies #π-calculus

π-Calculus, Dialogue Games and PCF (JMEH, CHLO), pp. 96–107.

CSL-1993-OngR #calculus #normalisation

A Generic Strong Normalization Argument: Application to the Calculus of Constructions (CHLO, ER), pp. 261–279.

TLCA-1993-HylandO #normalisation #proving

Modified Realizability Toposes and Strong Normalization Proofs (JMEH, CHLO), pp. 179–194.

ICALP-1992-Ong #lazy evaluation #modelling #λ-calculus

Lazy λ Calculus: Theories, Models and Local Structure Characterization (CHLO), pp. 487–498.

ASE-2017-TianDDO #effectiveness #model checking

More effective interpolations in software model checking (CT, ZD, ZD, CHLO), pp. 183–193.

ESOP-2016-DOsualdoO #communication #on the #π-calculus

On Hierarchical Communication Topologies in the π-calculus (ED, CHLO), pp. 149–175.

ESOP-2017-Cotton-BarrattM #branch #ml

ML and Extended Branching VASS (CCB, ASM, CHLO), pp. 314–340.

ESOP-2019-Alvarez-Picallo #datalog #fixpoint #incremental #recursion #semantics

Fixing Incremental Computation - Derivatives of Fixpoints, and the Recursive Semantics of Datalog (MAP, AET, MPJ, CHLO), pp. 525–552.

POPL-2016-HagueKO #automaton #bound #higher-order

Unboundedness and downward closures of higher-order pushdown automata (MH, JK, CHLO), pp. 151–163.

POPL-2018-BurnOR #higher-order #horn clause #verification

Higher-order constrained horn clauses for verification (TCB, CHLO, SJR), p. 28.