Search Results

Documents authored by Ong, C.-H. Luke

Found 2 Possible Name Variants:

Ong, C.H. Luke

Document
DOI: 10.4230/LIPIcs.RTA.2011.187
Improved Functional Flow and Reachability Analyses Using Indexed Linear Tree Grammars

Authors: Jonathan Kochems and C.H. Luke Ong

Published in: LIPIcs, Volume 10, 22nd International Conference on Rewriting Techniques and Applications (RTA'11) (2011)

Abstract
The collecting semantics of a program defines the strongest static property of interest. We study the analysis of the collecting semantics of higher-order functional programs, cast as left-linear term rewriting systems. The analysis generalises functional flow analysis and the reachability problem for term rewriting systems, which are both undecidable. We present an algorithm that uses indexed linear tree grammars (ILTGs) both to describe the input set and compute the set that approximates the collecting semantics. ILTGs are equi-expressive with pushdown tree automata, and so, strictly more expressive than regular tree grammars. Our result can be seen as a refinement of Jones and Andersen's procedure, which uses regular tree grammars. The main technical innovation of our algorithm is the use of indices to capture (sets of) substitutions, thus enabling a more precise binding analysis than afforded by regular grammars. We give a simple proof of termination and soundness, and demonstrate that our method is more accurate than other approaches to functional flow and reachability analyses in the literature.
Cite as

Jonathan Kochems and C.H. Luke Ong. Improved Functional Flow and Reachability Analyses Using Indexed Linear Tree Grammars. In 22nd International Conference on Rewriting Techniques and Applications (RTA'11). Leibniz International Proceedings in Informatics (LIPIcs), Volume 10, pp. 187-202, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2011)

Copy BibTex To Clipboard

@InProceedings{kochems_et_al:LIPIcs.RTA.2011.187,
  author =	{Kochems, Jonathan and Ong, C.H. Luke},
  title =	{{Improved Functional Flow and Reachability Analyses Using Indexed Linear Tree Grammars}},
  booktitle =	{22nd International Conference on Rewriting Techniques and Applications (RTA'11)},
  pages =	{187--202},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-30-9},
  ISSN =	{1868-8969},
  year =	{2011},
  volume =	{10},
  editor =	{Schmidt-Schauss, Manfred},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2011.187},
  URN =		{urn:nbn:de:0030-drops-31167},
  doi =		{10.4230/LIPIcs.RTA.2011.187},
  annote =	{Keywords: Flow analysis, reachability, collecting semantics, higher-order program, term rewriting, indexed linear tree grammar}
}

Ong, C.-H. Luke

Document
DOI: 10.4230/LIPIcs.LICS.2026.83
Contextual MetaML: Syntax and Full Abstraction

Authors: Haoxuan Yin, Andrzej S. Murawski, and C.-H. Luke Ong

Published in: LIPIcs, Volume 380, 41st Annual Symposium on Logic in Computer Science (LICS 2026)

Abstract
MetaML-style metaprogramming languages allow programmers to construct, manipulate and run code. In the presence of higher-order references for code, ensuring type safety is challenging, as free variables can escape their binders. In this paper, we present Contextual MetaML, the first metaprogramming language that supports storing and running open code under a strong type safety guarantee. The type system utilises contextual modal types to track and reason about free variables in code explicitly. A crucial concern in metaprogramming-based program optimisations is whether the optimised program preserves the meaning of the original program. Addressing this question requires a notion of program equivalence and techniques to reason about it. In this paper, we provide a semantic model that captures contextual equivalence for Contextual MetaML, establishing the first full abstraction result for an imperative MetaML-style language. Our model is based on traces derived via operational game semantics, where the meaning of a program is modelled by its possible interactions with the environment. We also establish a novel closed instances of use theorem that accounts for both call-by-value and call-by-name closing substitutions.
Cite as

Haoxuan Yin, Andrzej S. Murawski, and C.-H. Luke Ong. Contextual MetaML: Syntax and Full Abstraction. In 41st Annual Symposium on Logic in Computer Science (LICS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 380, pp. 83:1-83:27, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{yin_et_al:LIPIcs.LICS.2026.83,
  author =	{Yin, Haoxuan and Murawski, Andrzej S. and Ong, C.-H. Luke},
  title =	{{Contextual MetaML: Syntax and Full Abstraction}},
  booktitle =	{41st Annual Symposium on Logic in Computer Science (LICS 2026)},
  pages =	{83:1--83:27},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-434-5},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{380},
  editor =	{Faggian, Claudia and Katoen, Joost-Pieter},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.LICS.2026.83},
  URN =		{urn:nbn:de:0030-drops-268708},
  doi =		{10.4230/LIPIcs.LICS.2026.83},
  annote =	{Keywords: Metaprogramming, operational game semantics, trace model, contextual modal type theory}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2020.32
The Difference λ-Calculus: A Language for Difference Categories

Authors: Mario Alvarez-Picallo and C.-H. Luke Ong

Published in: LIPIcs, Volume 167, 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020)

Abstract
Cartesian difference categories are a recent generalisation of Cartesian differential categories which introduce a notion of "infinitesimal" arrows satisfying an analogue of the Kock-Lawvere axiom, with the axioms of a Cartesian differential category being satisfied only "up to an infinitesimal perturbation". In this work, we construct a simply-typed calculus in the spirit of the differential λ-calculus equipped with syntactic "infinitesimals" and show how its models correspond to difference λ-categories, a family of Cartesian difference categories equipped with suitably well-behaved exponentials.
Cite as

Mario Alvarez-Picallo and C.-H. Luke Ong. The Difference λ-Calculus: A Language for Difference Categories. In 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 167, pp. 32:1-32:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{alvarezpicallo_et_al:LIPIcs.FSCD.2020.32,
  author =	{Alvarez-Picallo, Mario and Ong, C.-H. Luke},
  title =	{{The Difference \lambda-Calculus: A Language for Difference Categories}},
  booktitle =	{5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020)},
  pages =	{32:1--32:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-155-9},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{167},
  editor =	{Ariola, Zena M.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2020.32},
  URN =		{urn:nbn:de:0030-drops-123549},
  doi =		{10.4230/LIPIcs.FSCD.2020.32},
  annote =	{Keywords: Cartesian difference categories, Cartesian differential categories, Change actions, Differential lambda-calculus, Difference lambda-calculus}
}
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2026 Schloss Dagstuhl – LZI GmbH Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact