M. Hague and C.-H. L. Ong, Winning Regions of Pushdown Parity Games: A Saturation Method. In Proceedings of CONCUR 2009, Bologna. Springer-Verlag LNCS, 2009.
D. Hopkins and C.-H. L. Ong, Homer: a Higher-order Observational equivalence Model checkER. In Proceedings of CAV 2009, Grenoble, Springer-Verlag LNCS, 2009.
C. Broadbent and C.-H. L. Ong, On Global Model Checking Trees Generated by Higher-Order Recursion Schemes. In Proceedings of 12th International Conference on Foundations of Software Science and Computational Structures (FOSSACS 2009) (Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2009, York, UK, March 22-29, 2009.) pp. 107-121, LNCS 5504 Springer 2009
Naoki Kobayashi and Luke Ong, Complexity of Model Checking Recursion Schemes for Fragments of the Modal Mu-Calculus. In Proceedings of ICALP 2009, Rhodes, Springer-Verlag LNCS, 2009. [Long version]
Naoki Kobayashi and Luke Ong, A Type System Equivalent to Modal Mu-Calculus Model Checking of Recursion Schemes. In Proceedings of 24th Annual IEEE Symposium on Logic in Computer Science (LICS 2009), Los Angeles, pp. Computer Society Press, 2009. To appear. [Long version]
C.-H. L. Ong and N. Tzevelekos, Functional Reachability. In Proceedings of 24th Annual IEEE Symposium on Logic in Computer Science (LICS 2009), Los Angeles, pp. Computer Society Press, 2009. To appear.
William Blum, C.-H. Luke Ong: The Safe Lambda Calculus. In Logical Methods in Computer Science, Volume 5, Issue 1, CoRR abs/0901.2399: (2009)
William Blum, C.-H. Luke Ong, A Concrete Presentation of Game Semantics. In Proceedings of the International Workshop on Games for Logic and Programming Languages (GaLoP 2009), a satellite workshop of ETAPS 2008, 2008.
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. Springer 2008.
C.-H. Luke Ong, Verification of Higher-Order Computation: A Game-Semantic Approach. In Proceedings of 17th European Symposium on Programming (ESOP 2008) (Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2008, Budapest, Hungary, March 29-April 6, 2008.) pp. 299-306, LNCS 4960, Springer 2008.
Arnaud Carayol, Matthew Hague, Antoine Meyer, C.-H. Luke Ong, Olivier Serre: Winning Regions of Higher-Order Pushdown Games. In Proceedings of 23rd Annual IEEE Symposium on Logic in Computer Science, pp. 193-204, Computer Society Press, 2008. [Long version]
Matthew Hague, Andrzej S. Murawski, C.-H. Luke Ong, Olivier Serre: Collapsible Pushdown Automata and Recursion Schemes. In Proceedings of 23rd Annual IEEE Symposium on Logic in Computer Science, pp. 452-461, Computer Society Press, 2008. [Long version]
Matthew Hague, C.-H. Luke Ong: Symbolic Backwards-Reachability Analysis for Higher-Order Pushdown Systems, Logical Methods in Computer Science, Volume 4, Issue 4, CoRR abs/0811.1103: (2008)
C.-H. Luke Ong. Hierarchies of Infinite Structures Generated by Pushdown Automata and Recursion Schemes. In Proceedings of 32nd International Symposium on Mathematical Foundations of Computer Science (MFCS 2007), Ceskż Krumlov, Czech Republic, August 26-31, 2007. pp. 15-21, LNCS 4708 Springer 2007,
W. Blum and C.-H. L. Ong. The Safe Lambda Calculus. In Proceedings of 8th International Conference on Typed Lambda Calculus and Applications (TLCA 2007), Paris, France, pp. 39-53, Springer-Verlag LNCS 4583, 2007.
M. Hague and C.-H. L. Ong. Symbolic backwards-reachability analysis of higher-order pushdown systems. In Proceedings of Tenth International Conference on Foundations of Software Science and Computation Structures (FoSSaCS 2007), 24 March - 1 April, 2007, Braga, Portugal, pp. 213-229, Springer-Verlag LNCS 4423, 2007.
S. Sanjabi and C.-H. L. Ong. Fully abstract semantics of additive aspects by translation . In Proceedings of Sixth International ACM Conference on Aspect-Oriented Software Development (AOSD 2007), Vancouver, British Columbia, March 12-16, 2007. pp. 135-148, 2007
S. Abramsky and C.-H. L. Ong. Algorithmic Game Semantics and its Application: Final Report of an EPSRC Project. 6 pages. January 2006.
C.-H. L. Ong. Some results on a game-semantic approach to the verification of infinite structures . In Proceedings of 20th International Workshop and 15th Annual Conference of the EACSL (CSL 2006), Szeged, Hungary, September 25-29, 2006, pages 31-40, Springer LNCS 4207, 2007
A. S. Murawski and C.-H. L. Ong. Fast verification of MLL proof nets via IMLL. ACM Transactions on Computational Logic, Volume 7, Number 3, pages 473-498, July 2006.
D. R. Ghica, A. S. Murawski and C.-H. L. Ong. Syntactic control of concurrency. Theoretical Computer Science 350 (2006) 234-251.
C.-H. L. Ong. On model-checking trees generating by higher-order recursion schemes, Preprint, 55 pp. 2006.
C.-H. L. Ong. On model-checking trees generating by higher-order recursion schemes (extended abstract). In Proceedings of 21st IEEE Symposium on Logic in Computer Science (LICS 2006), pages 81-90, Computer Society Press, 2006.
C.-H. L. Ong. Computer Science Logic: 19th International Workshop and 14th Annual Conference of the EACSL, Oxford, UK, August 22-25, 2005. Proceedings (CSL 2005), LNCS Volume 3634, Springer, 2005.
A. S. Murawski, C.-H. L. Ong and I. Walukiewicz, Idealized Algol with Ground Recursion, and DPDA Equivalence. In Proceedings of the 32nd International Colloquium on Automata, Languages and Programming (ICALP 2005), LNCS Volume 3580, pp. 917-929, Springer-Verlag, 2005. [ps]
K. Aehlig, J. G. de Miranda and C.-H. L. Ong. The monadic second order theory of trees given by arbitrary level-2 recursion schemes is decidable. In Typed Lambda Calculi and Applications: 7th International Conference (TLCA 2005), Nara, Japan, April 21-23, 2005. Proceedings, pp. 39-54, LNCS Volume 3461, Springer, 2005.
K. Aehlig, J. G. de Miranda and C.-H. L. Ong. Safety is not a restriction at level 2 for string languages. In Foundations of Software Science and Computational Structures: 8th International Conference (FoSSaCS 2005). Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2005, Edinburgh, UK, April 4-8, 2005. Proceedings, pp. 490-504, LNCS Volume 3441, Springer, 2005.
C.-H. L. Ong, An approach to deciding observational equivalence of Algol-like languages. Annals of Pure and Applied Logic, 130: 125-171, 2004. [ps.gz ]
K. Aehlig, J. G. de Miranda and C.-H. L. Ong. Safety is not a restriction at level 2 for string languages. OUCL Technical Report PRG-RR-04-23, 2004. [full version ps.gz]
D. R. Ghica, A. S. Murawski and C.-H. L. Ong. Syntactic control of concurrency. In Proceedings of 31st International Colloquium on Automata, Languages and Programming (ICALP 2004), Turku, Finland, 2004, LNCS Volume 3142, pp. 683-69, Springer-Verlag, 2004. [conference ps, full version ps ]
S. Abramsky, D. R. Ghica, A. S. Murawski, C.-H. L. Ong and I. D. R. Stark. Nominal games and full abstraction for the nu-calculus. In Proceedings of 19th Annual IEEE Symposium in Logic in Computer Science (LICS 2004), Turku, Finland, 2004, pp. 150-159, Computer Science Press, 2004. [ps ]
S. Abramsky, D. R. Ghica, A. S. Murawski and C.-H. L. Ong. Applying Game Semantics to Compositional Software Modeling and Verifications. In Proceedings of 10th International Conference on Tools and Algorithms for the Construction and Analysis of System (TACAS 2004), Barcelona, March 2004. LNCS Vol. 2988, Springer-Verlag, 2004, pages 421-435. [ps ]
A. S. Murawski and C.-H. L. Ong, On the interpretation of Safe Recursion in Light Logic. In Theoretical Computer Science, 318, pp. 197-223, 2004. [ps]
C.-H. L. Ong and P. di Gianantonio. Games characterizing Levy-Longo trees. In Theoretical Computer Science 312, pp. 121-142, 2004.
S. Abramsky, D. Ghica, C.-H. L. Ong and A. Murawski. Algorithmic game semantics and component based verification. In Proceedings of Workshop on Specification and Verification of Component-Based Systems (SAVCBS 2003), Helsinki, September 2003.
A. D. Ker, H. Nickau and C.-H. L. Ong, Adapting innocent game models for the Boehm tree lambda-theory. In Theoretical Computer Science 308, pp. 333-366, 2003.
A. S. Murawski and C.-H. L. Ong, Exhausting Strategies, Joker Games and Full Completeness for IMLL with Unit. In Theoretical Computer Science 294, pp. 269-305, 2003. [Science Direct (pdf)]
A. D. Ker, H. Nickau and C.-H. L. Ong, Innocent game models of untyped lambda calculus. In Theoretical Computer Science 272, pp. 247-292, 2002. [Abstract | ps.gz (revised Sep 99)]
C.-H. L. Ong, Observational Equivalence of Third-order Idealized Algol is decidable. In Proceedings of IEEE Symposium on Logic in Computer Science (LICS 2002), 22-25 July 2002, Copenhagen Denmark, pages 245-256, Computer Society Press, 2002. [Abstract | ps.gz]
A. Basu, C.-H. L. Ong, A. Rasala, B. Shepherd and G. Wilfong, Route Oscillation in I-BGP. In Proceedings of Annual Conference of the ACM Special Interest Group on Data Communications (SIGCOMM 2002), pp. 235-247, August 29-23, Pittsburgh, USA, ACM Press, 2002. [Abstract | ps.gz]
C.-H. L. Ong, Model checking Algol-like languages using Game Semantics . In Proceedings of 22nd Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2002), Kanpur, India, 12-14 December 2002, LNCS, Springer-Verlag, 2002.
C.-H. L. Ong and P. de Gianantonio, Games characterizing Levy-Longo trees. In Proceedings of 29th International Colloquium on Automata, Languages and Programming (ICALP 2002), M\'alaga, Spain, July 2002, pages 476-487, Springer-Verlag, 2002. LNCS Volume 2380. [Abstract | ps.gz]
A. S. Murawski and C.-H. L. Ong, Evolving games and essential nets for affine polymorphism. Proceedings of Conference on Typed Lambda Calculi and Applications (TLCA 2001), Kraków, Poland, May 2-5, 2001, Springer-Verlag, Lecture Notes in Computer Science Vol. 2044, pages 360-375, 2001. [Abstract | ps.gz]
C.-H. Luke Ong, Light Logic and Resource Bounded Computation.. In Proceedings of the First Asian Workshop on Programming Languages and Systems (APLAS 2000), National University of Singapore, Singapore, December 18-20, 2000.
J. M. E. Hyland and C.-H. L. Ong, On Full Abstraction for PCF: I. Models, observables and the full abstraction problem, II. Dialogue games and innocent strategies, III. A fully abstract and universal game model. In Information and Computation, Volume 163, pp. 285-408, December 2000. [Abstract | ps.gz ]
A. S. Murawski and C.-H. L. Ong, SLR- is PTIME complete. 5 pages, 2000. [Abstract | ps.gz]
A. S. Murawski and C.-H. L. Ong, Can safe recursion be interpreted in light logic?. Paper presented at the (LICS affiliated) Second International Workshop on Implicit Computational Complexity, Santa Barbara, California, 29-30 June 2000. 20 pages. [Abstract | ps.gz]
A. S. Murawski and C.-H. L. Ong, Discreet Games, Light Affine Logic and PTIME Computation. In Proceedings of Annual Conference of the European Association of Computer Science Logic (CSL 2000), August 2000, Fischbachau, Germany, pages 427-441. LNCS Volume 1862, Springer-Verlag, 2000. [Abstract | ps.gz]
A. S. Murawski and C.-H. L. Ong, Dominator Trees and Fast Verification of Proof Nets. In Proceedings of 15th IEEE Annual Symposium on Logic in Computer Science (LICS 2000), June 26-29, 2000, Santa Barbara, California. IEEE Computer Society Press, pp 181-191, 2000. [Abstract | ps.gz]
A. D. Ker, H. Nickau and C.-H. L. Ong, A universal innocent game model for the Boehm tree lambda theory. Programming Research Group Technical Report TR-10-00, November 2000. [Abstract | ps.gz]
A. S. Murawski and C.-H. L. Ong, A Linear-time Algorithm for Verifying MLL Proof Nets via Essential Nets. In Davis, Roscoe and Woodcock (editors), Millennial Perspectives in Computer Science: Proceedings of the 1999 Oxford-Microsoft Symposium in Honour of Sir Tony Hoare, pages 289-302, Cornerstones of Computing, MacMillan, 2000. [Abstract | ps.gz]
C.-H. L. Ong, Operational and Denotational Semantics of PCF. Notes for a course of the Summer School on Semantics of Computation at BRICS, University of Aarhus, Denmark, 3-7 May 1999, 51 pp., 1999. [Abstract | ps.gz]
A. S. Murawski and C.-H. L. Ong, Exhausting Strategies, Joker Games and Full Completeness for IMLL with Unit. In Proceedings of the 8th Conference on Category Theory and Computer Science (CTCS 1999), Edinburgh, September 1999, Electronic Notes in Theoreotical Computer Science 29, 31 pages, 1999. [Abstract | (PostScript 269.8 Kb)]
T. W. Koh and C.-H. L. Ong, Explicit Substitution Internal Languages for Autonomous and *-Autonomous Categories (Preliminary version). In Proceedings of the 8th Conference on Category Theory and Computer Science (CTCS 1999), Edinburgh, September 1999, Electronic Notes in Theoreotical Computer Science 29, 30 pages, 1999. [Abstract | (PostScript 285.7 Kb).]
A. D. Ker, H. Nickau and C.-H. L. Ong, A universal innocent game model for the Boehm tree lambda theory. In Computer Science Logic: Proceedings of the 8th Annual Conference on the EACSL (CSL 1999) Madrid, Spain, September 1999, LNCS Volume 1683, Springer-Verlag, pp. 405-419, 1999. [Abstract | ps.gz]
T. W. Koh and C.-H. L. Ong, Type theories for autonomous and *-autonomous categories: I. Types theories and rewrite systems II. Internal languages and coherence theorems . Preprint, 65 pp., 1998. [Abstract | ps.gz]
C.-H. L. Ong and C. A. Stewart, A Curry-Howard Foundation for functional computation with control. In Proceedings of ACM SIGPLAN-SIGACT Symposium on Principle of Programming Languages (POPL 1997), Paris, January 1997, ACM Press, pp. 215-227, 1997. [Abstract | ps.gz]
C.-H. L. Ong, A semantic view of classical proofs: type-theoretic, categorical, denotational characterizations. In Proceedings of 11th IEEE Annual Symposium on Logic in Computer Science (LICS 1996), IEEE Computer Society Press, pp. 230-241, 1996. [Abstract | ps.gz]
J. M. E. Hyland and C.-H. L. Ong, Pi-calculus, dialogue games and PCF In Proceedings of the 7th ACM Conference on Functional Programming Languages and Computer Architecture (FPCA 1995), pages 96-107, ACM Press, 1995. [Abstract | ps.gz]
C.-H. L. Ong, Correspondence between Operational and Denotational Semantics. In Handbook of Logic in Computer Science, Volume 4, edited by S. Abramsky, D. Gabbay and T. S. E. Maibaum, Oxford University Press, pages 269-356, 1995. [Abstract | ps.gz]
C.-H. L. Ong and E. Ritter, A Generic Strong Normalization Proof: Application to the Calculus of Constructions (Extended abstract). In Computer Science Logic: 7th Workshop, Swansea, UK, September 1993, Selected Papers (CSL 1993), Lecture Notes in Computer Science Volume 832, Springer-Verlag, pp. 261-279, 1994. [Abstract | ps.gz]
J. M. E. Hyland and C.-H. L. Ong, Modified Realizability Topos and Strong Normalization Proofs (Extended abstract). In Proceedings of Typed Lambda Calculus and Applications (TLCA 1993), Utrecht, March 1993, Lecture Notes in Computer Science Volume 664, Springer-Verlag, pages 179-194, 1993. [Abstract | ps.gz]
C.-H. L. Ong, Non-Determinism in a Functional Setting. In Proceedings of 8th IEEE Annual Symposium on Logic in Computer Science (LICS 1993), Montreal, Canada, 1993, pages 275-286, 1993. [Abstract | ps.gz]
J. M. E. Hyland and C.-H. L. Ong, Fair Games and Full Completeness for Multiplicative Linear Logic without the Mix-Rule. Preprint, 25 pp., 1993. [Abstract | ps.gz]
S. Abramsky and C.-H. L. Ong, Full Abstraction in the Lazy Lambda Calculus: I, II. In Information and Computation 105, pages 159-267, 1993. [Abstract | ps.gz]
C.-H. L. Ong, Lazy Lambda Calculus: Theories, Models and Local Structure Characterization. In Proceedings of 19th International Colloquium on Automata, Programming and Languages (ICALP 1992), Springer-Verlag, Lecture Notes in Computer Science Volume 623, 1992. [Abstract | ps.gz]
C.-H. L. Ong, Fully Abstract Models of the Lazy Lambda Calculus. In Proceedings of 29th IEEE Conference on Foundations of Computer Science (FOCS 1988), pages 368-376, IEEE Computer Society Press, 1988.
To satisfy the conditions of certain publishers regarding distribution of my papers on the web, I have been advised to include the following:
The documents contained in these directories are included by the contributing authors as a means to ensure timely dissemination of scholarly and technical work on a non-commercial basis. Copyright and all rights therein are maintained by the authors or by other copyright holders, notwithstanding that they have offered their works here electronically. It is understood that all persons copying this information will adhere to the terms and constraints invoked by each author's copyright. These works may not be reposted without the explicit written permission of the copyright holder.