My Research

C.-H. L. Ong

I have been an active researcher in Theoretical Computer Science since the completion of my PhD in 1988, apart from a two-year gap performing National Service in Singapore. My work has mainly been in Semantics of Computation, which is concerned with the development and analysis of mathematical structures that model computation (such as programming languages and concepts) using ideas and tools from Mathematical Logic, with a view to the development of methods and principles for reasoning about program properties.

Research achievements

The following is an edited list of my research contributions from 1988 to 2001, spanning several areas in Semantics:

My doctoral thesis was an extensive study of the Lazy Lambda Calculus, a prototypical formalism for Functional Programming. The work was the first to address systematically the mismatch between the ``standard'' (i.e. sensible) theory of the classical Lambda Calculus and the common practice of lazy functional programming. On the basis of the thesis, I was awarded a Prize Fellowship at Trinity College, Cambridge. The thesis led to the publication of a 108-page monograph (with Abramsky) [1] in the leading journal Information and Computation, and refereed articles in the proceedings of several top-ranked Theoretical Computer Science conferences such as FOCS, LICS and ICALP [14,16,15]. Some highlights: construction of fully abstract models for several lazy $\lambda$-calculi, and non-full abstraction results; a new ordering (called lazy PSE-ordering) between untyped terms, and an associated local structure theorem; a proof system for a lazy $\lambda$-calculus based on Scott's logic of existence that is sound and complete for a class of partial categories.

Types in modern programming languages are one of the best examples of a truly useful application of Logic to Computer Science. A desirable property of any type theory is strong normalization, which is of fundamental importance because it gives a way to establish consistency. Unfortunately the standard method to prove strong normalization is a highly complex and unwieldy syntactic argument. A focus of my postdoc years at Cambridge was an abstract and generic treatment of strong normalization proofs. With Hyland, I have shown that an appropriate quotient of the strongly normalizing $\lambda$-terms is an instance of a new kind of applicative algebra, called conditionally partial combinatory algebra. Any such algebra gives rise to a tripos, which in turn determines a topos, provided the underlying intuitionistic predicate logic is interpreted in the style of Kreisel's Modified Realizability. A powerful generic strong normalization argument (for a class of dependent and impredicative type theories) can then be assembled from two type-erasure lemmas in the framework of the topos. This has been applied to System F and the Calculus of Constructions [3,21].

Game Semantics is a way of giving meanings to computation by viewing the interactive process of computation as game playing. With Hyland, I have produced the first syntax-independent fully abstract model of PCF. The result characterizes a notion of computability at higher types, and solves a long-standing open problem in the Semantics of Programming Languages. Our work, as reported in a 123-page monograph in Information and Computation [5], (together with the work of Abramsky et al.) opened up the field of Game Semantics. Our version of games, now known as Hyland-Ong games, and the notion of innocent strategies are the basis of an impressive programme by Abramsky and his co-workers to classify and analyse the ``space of programming languages'' systematically around the Semantic Cube. An exact representation of the innocent style of interaction has been given using the $\pi$-Calculus [4]. The other main strand of my work in Game Semantics has been the construction of accurate models for (pure) lambda calculi, both untyped and polymorphically typed versions. Ker, Nickau and I have given the first syntax-independent universal game models for the untyped $\lambda$-calculus, characterizing the maximal consistent sensible theory and B "ohm-tree theory [6] using a notion of effectively almost-everywhere copycat strategies. See also [20]. We have extended both the innocent and history-free game semantics to construct fully complete models for 2nd-order polymorphic $\lambda$-calculus and affine logic respectively using a notion of evolving games [12].

Linear Logic has been a recurrent theme of my research in Semantics. Using a notion of fair games, Hyland and I have constructed the first fully complete model of Multiplicative Linear Logic (without MIX). Murawski and I have studied the knotty problem of representing Linear Logic proofs with units, and characterized the intuitionistic system in terms of essential nets, joker games [13], and an explicit-substitution internal language of $\ast$-autonomous categories [7]. A recent direction concerns algorithmic properties of proof nets: we have developed linear-time algorithms for verifying linear logic formulas [8]; a particularly intuitive and simple such algorithm based on dominator trees has appeared in LICS 2000 [10]. My other main direction in Proof Theory in Computer Science concerns the computational meaning of classical proofs and connexions with functional control operators. I have given the first categorical characterization and game semantics of classical proofs (as formalized by Parigot's $\lambda\mu$-calculus) in LICS 1996 [17], and studied (with student Stewart) both call-by-name and call-by-value versions of a family of functional languages with control operators that are descendants of the $\lambda\mu$-calculus in POPL 1997 [22].

Research since 2002: from Structures to Algorithmics

More recently my research has tended to be motivated by problems of an algorithmic nature. For many decades the two branches of Theoretical Computer Science, Structures (Semantics and Logic) and Algorithmics (Algorithms and Complexity), have flourished separately, with little interaction between the two. A general theme is to establish connexions between the two by studying problems that can benefit from a cross-fertilization of ideas and techniques. The following is a summary of achievements in three topics in this direction since 2002:

Algorithmic Game Semantics and Software Model Checking A notable success in Computer Science over the past two decades has been the development of techniques for the computer-assisted verification of finite-state systems. These methods, especially Model Checking, apply with such great effect to relatively ``flat'' unstructured processes, such as digital hardware design and the analysis of communication protocols, that they are now standard development tools in Industry. In contrast, Software Model Checking, the application of these techniques to computer software, has been less successful: Programs are potentially infinite-state systems, and key programming features such as data types, control flow, higher-order constructs and bindings of various kinds can only be accurately modelled using highly-structured mathematical models, as studied in Semantics. With Abramsky, Ghica, McCusker and Murawski, I have proposed a novel approach to Software Model Checking based on Game Semantics. Game Semantics provides a very concrete way of building highly accurate models for a wide range of advanced programming languages (as the various full abstraction results show); it has a clear operational content, while admitting compositional methods in the style of denotational semantics. The basic objects studied in Game Semantics (i.e. games and strategies) can be seen as certain kinds of highly-constrained processes, and hence admit the same kind of automata-theoretic representations central to model checking and allied methods in computer-assisted verification.

By a careful encoding of justification pointers and state, I have shown that the fully-abstract strategy denotation of any recursion-free 3rd-order Idealized Algol term can be represented as a deterministic pushdown automaton (DPDA). As a pleasing consequence, observational equivalence for this fragment reduces to the famous problem of DPDA EQUIVALENCE ("Given two DPDAs, do they recognize the same language?") which has only recently been shown to be decidable by S 'enizergues (who was awarded the G "odel Prize 2002 for his accomplishment). This gives a new method for model-checking a wide range of behavioural properties of Idealized Algol and other cognate higher-order procedural programs. A distinctive of our approach is that it yields compositional verifiers that are sound and complete, and fully automatic, for languages that have a fully abstract game semantics. The results are published in LICS 2002 [18]. I have since been invited to lecture on the work at international conferences and workshop in Paris (Jul '04), India (Dec '02) and Rome (Feb '03), and at specialist games workshops in Ottawa (Jun '03) and Vienna (Aug '03) (see §  for an update list of invited talks). A full account of my approach to Algorithmic Game Semantics (63 pages) has been submitted by invitation to Annals of Pure and Applied Logic, and accepted to appear in 2004 [19].

Implicit computational complexity Implicit computational complexity is concerned with the intrinsic understanding of complexity classes, without recourse to any computational cost model or notion of resource measure, and in terms of such ``neutral'' systems as logic or programming languages or abstract semantic structures. My work here concerns the complexity class PF of polytime-computable numeric functions. I have worked on a programme (with student Murawski) to give a game-semantic characterization of PF by constructing fully complete models for increasingly rich fragments of Girard's system of Light Logics [9,12]. This has led to a fully complete model of Light Affine Logic, which may be considered an accurate denotational model of PF, and a full account is in preparation. More recently we have studied, in a paper [11] to appear in the journal Theoretical Computer Science, the relationship between Light Affine Logic and Bellantoni-Cook function algebra $\textit{BC}$, which is another intrinsic characterization of PF. We have considered the question of the extent to which one system can be interpreted in the other. I have contributed to the International Workshop on Implicit Computational Complexity both by research, and as a member of the Steering Committee (since Dec'02).

Internet routing protocol The Border Gateway Protocol (BGP) is the de facto standard inter-domain routing protocol in the Internet. Though much of the Internet depends on it (BGP version 4 governs the exchange of reachability information between Internet Service Providers), it is perhaps surprising that BGP is not safe: BGP4 does not guarantee that any given network configuration will converge, even in the absence of network topology changes. In collaboration with Basu, Shepherd and Willfong from Bell Laboratories and Rasala at MIT, I have proposed a formal model of Internal-BGP and used it to show that even deciding whether an I-BGP configuration can converge is an NP-complete problem. We have proposed a modification to I-BGP by improving a router's ability to choose the best path for sending data packets, and shown that the modified protocol always converges, even when route reflection (a standard method to configure I-BGP routers efficiently for large networks) is used. Moreover, it converges to the same stable routing configuration, regardless of the order in which messages are sent or received. Our work has been published in the refereed proceedings of ACM SIGCOMM 2002 [2], which is widely acknowledged as the first-ranked conference in Computer Communications. We have submitted an invited proposal to the Internet standards body IETF, and an application for a U.S. patent in connexion with the discovery has been lodged. The work has received commendation from the President of Bell Labs Research and Advanced Technologies, and was cited as a model of Bell Lab's Mission of Collaboration ¹.

Space-bounded computation and region analysis [28]; algorithmic game semantics and software model checking [26]; convergence properties of Internet inter-domain routing protocol BGP [23].

Future plan: New Approaches to Software Verification

For the next three years or so, I intend to work in the same three areas (broadly interpreted) identified above, consolidating existing lines of enquiry and developing certain themes further.

Abramsky and I are co-PIs of an EPSRC project Algorithmic Game Semantics and its Application (Aug 2002 - July 2005), employing Ghica and Murawski as postdocs. Much has already been achieved. Among the remaining tasks, I intend to work on questions of decidability of observational equivalence for low-order fragments of call-by-value Idealized Algol with recursion. This problem is of strategic importance from the perspective of Software Model Checking, since the fragment can embed almost all of the language C (except pointer structures). It is tricky to analyse call-by-value games algorithmically. The plan is to begin with simpler fragments (e.g. only considering procedures that may pass parameters by value but not by reference). Another goal, in collaboration with Ranko Lazic at Warwick, is to enable compositional verification of programs and specifications which contain large, polymorphic or infinite data types using ideas from symbolic model checking and other techniques such as symmetry elimination, and well-quasi ordering on states. This has not been addressed in the context of Game Semantics so far, but is necessary for the approach to scale to model checking industrial software. With Ian Stark at Edinburgh, I intend to work on a fully abstract (game) model for Reduced ML with reference testing (we think of it as the non-objective part of the influential ML-dialect OCAML) and its algorithmic representation, with a view to extracting algorithms for deciding observational equivalence of appropriate fragments.

I believe a strategic direction of research in Software Verification is to combine insights and results from Semantics of Programming Languages with recent advances in verification techniques for infinite-state systems. I have a research plan in collaboration with Colin Stirling at Edinburgh to develop automatic techniques that deal directly with infinite-state systems which are accurate computation models of Algol-like Higher-order Procedural Languages (or HOPL). Recently, there has been considerable activity in the study of classification and algorithmic properties of infinite-state systems. The hope is that successful algorithmic techniques such as model checking and equivalence checking can be transferred from finite to classes of infinite-state systems. A striking example is pushdown automata and transition graphs determined by them. M "uller and Schupp have proved that the monadic 2nd-order (MSO) theory of the transition graph of a pushdown automaton is decidable. Another development is the positive solution, by S 'enizergues, to the long standing open problem of DPDA EQUIVALENCE, as mentioned earlier.

We shall consider the verification of recursively-defined HOPL programs. The problem is pertinent because a great many useful programs written in Algol-like languages belong to this class. Unfortunately observational equivalence of recursive IA terms, even when restricted to 2nd-order, is undecidable [18,19]. A question that follows naturally is: what properties are decidable for this important class? There is an old model for such programs, namely, higher-order recursion schemes, as defined by Damm in the 1970s. A recursion scheme is given by a finite set of higher-order recursive tree equations, such as $F\,y\,z = f(F\,y\, (yz), yz)$ and a starting configuration, such as $F\, g \, a$. A scheme generates a possibly infinite (finite-branching) tree, whose nodes are labelled by first-order symbols. The example generates the tree that is the limit of the sequence

$$f(F\, g\, (ga), ga), f(f(F \, g \, (g(ga)), g(ga)),ga), \cdots.$$

Such trees are a canonical representation of a class of higher-order recursively defined functional programs by an infinite process of unfolding. (The order of a scheme is the highest order of symbols in $F$: in the example $F$ is order-$2$.) They define an infinite hierarchy of finitely-presentable infinite-state systems; we propose to study the verification problem in this more general and abstract setting.

Remarkably Knapik et al. have recently shown that all trees generated by higher-order recursion schemes (of any order), satisfying a technical constraint called safety, have decidable MSO theories. An example of the kind of properties that can be expressed in the powerful MSO logic (or a temporal sublogic, such as modal $\mu$-calculus) about a tree generated by a scheme is ``there are finitely many occurrences of $x$ in some subtree rooted at $f$'' where $x$ and $f$ are symbols used to label nodes. The decidability of such properties is of relevance to Program Analysis (e.g. usage analysis and strictness analysis). Knapik et al. have characterized safe higher-order trees in terms of higher-order pushdown automata. A higher-order pushdown automaton consists of a finite-control and a higher-order stack. An order-$1$ stack (as in a DPDA) is just a sequence of stack symbols and an order-$2$ stack is a sequence of order-$1$ stacks, and so on for higher-orders. Higher-order push and pop operations introduce and reduce lower-order substacks. The need for higher-order stacks is to capture the way higher-order variables bind arguments. There are several intriguing open problems: Is every higher-order recursion scheme equivalent to a safe one? Are the traces at each level of the hierarchy context-free? Are the non-deterministic trees more expressive (and if so, at which levels)? We also plan to investigate the properties of a new kind of automata that has a pushdown stack containing structures with pointers (to items in the stack). Such automata are easily seen to be equivalent to (unrestricted) higher-order recursion scheme. The key question is its relationship with higher-order pushdown automata. We hope to be able to use the new automaton to resolve the question of whether the safety constraint is really necessary for MSO decidability.

Other plans

A provably safe version of BGP may yet fail to deliver effective connectivity by its inability to scale up, as the Internet continues along a path of inexorable growth (e.g. BGP global routing tables have doubled in size each year, over the past three to four years). Our current aim is to address scalability issues of the I-BGP oscillation-eliminating algorithm both theoretically, by a mathematical analysis of our model; and experimentally, by the construction of a detailed simulation of the interaction between routers for the purpose of performance prediction. This work will be funded in part by Bell Laboratories.

We aim to find versions of Light Affine Logic and Bellantoni and Cook's $BC$ that characterize space complexity classes such as L (Logspace), NL (Non-deterministic Logspace), NP and PSPACE. A priority is to examine the ``feasible'' space complexity classes: L and NL. In joint work with Mairson, we have shown that numeric functions definable in $BC^-$ (a linear version of $BC$ introduced in [11]) are L-computable because of an invariance. (By the invariance, we can infer, for instance, that the definition-by-case construct and the even-shift functions in [28] are not definable in $BC^-$.) A natural question is to find out what needs to be added to $BC^-$ to make it L-complete or NL-complete. (It seems highly unlikely that $BC^-$ functions are NC(1)-computable.) A difficulty has to do with the fact that L-computable numeric functions may well return results that are polynomially long. As a first approximation, we will look at functions in L that have ``short'' ($\log{n}$-sized) output.

Bibliography

1

S. Abramsky and C.-H. L. Ong.
Full abstraction in the Lazy Lambda Calculus.
Information and Computation, 105:159-267, 1993.

2

A. Basu, C.-H. L. Ong, A. Rasala, F. B. Shepherd, and G. Wilfong.
Route oscillation in I-BGP.
page 11 pages. ACM Press, 2002.
Proceedings of ACM SIGCOMM 2002 Conference (Applications, Technologies, Architectures,and Protocols for Computer Communication), August 29-23, 2002.

3

J. M. E. Hyland and C.-H. L. Ong.
Modified realizability topos and strong normalization proofs.
In Proc. Conf. Typed Lambda Calculus and Applications, Utrecht, March 93, pages 179-194. Springer-Verlag, 1993.
LNCS Vol. 664.

4

J. M. E. Hyland and C.-H. L. Ong.
Pi-calculus, dialogue games and PCF.
In Proc. 7th ACM Conf. Functional Prog. Lang. Comp. Architecture, pages 96 - 107. ACM Press, 1995.

5

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.
Information and Computation, 163:285-408, 2000.

6

A. D. Ker, H. Nickau, and C.-H. L. Ong.
Innocent game models of untyped $\lambda$-calculus.
Theoretical Computer Science, 272:247-292, 2002.

7

T. W. Koh and C.-H. L. Ong.
Explicit substitution internal languages for autonomous and $\ast$-autonomous categories.
Electronic Notes in Theoretical Computer Science, 29, 1999.
Proceedings of the 8th Conf. on Category Theory and Computer Science 1999, 30 pp.

8

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. McMillan, 2000.
Cornerstones of Computing.

9

A. S. Murawski and C.-H. L. Ong.
Discreet games, Light Affine Logic and PTIME computation.
In Proceedings of CSL2000, Annual Conference of the European Association of Computer Science Logic, August 2000, Fischbachau, Germany., pages 427-441. Springer-Verlag, 2000.
LNCS Vol. 1862.

10

A. S. Murawski and C.-H. L. Ong.
Dominator trees and fast verification of proof nets.
In Proceedings of 15th IEEE Symposium on Logic in Computer Science, pages 181-191. IEEE Computer Society Press, 2000.

11

A. S. Murawski and C.-H. L. Ong.
Can safe recursion be interpreted in light logic?
Presented at the Second International Workshop on Implicit Computational Complexity, Santa Barbara, California, 29 - 30 June 2000; submitted to Theoretical Computer Science, 31 pages, April 2001.

12

A. S. Murawski and C.-H. L. Ong.
Evolving games and essential nets for affine polymorphism.
In Typed Lambda Calculi and Applications: Proc. 5th Int. Conf. TLCA2001, Krakow, Poland, May 2001, pages 360-375. Springer-Verlag, 2001.
LNCS Vol. 2044.

13

A. S. Murawski and C.-H. L. Ong.
Exhausting Strategies, Joker Games and Full Completeness for IMLL with Unit.
Theoretical Computer Science, 294:269-305, 2003.

14

C.-H. L. Ong.
Fully abstract models of the lazy lambda calculus.
In Proc. 29th Conf. Foundations of Computer Science, pages 368-376. IEEE Computer Society Press, 1988.

15

C.-H. L. Ong.
Lazy lambda calculus: Theories, models and local structure characterization.
In Proc. 19th Int. Coll. Automata, Programming and Languages. Springer, 1992.
LNCS Vol. 623.

16

C.-H. L. Ong.
Non-determinism in a functional setting-extended abstract.
In Proc. 8th IEEE Annual Symp. Logic in Computer Science, Montreal, Canada, pages 275-286. IEEE Computer Society Press, 1993.

17

C.-H. L. Ong.
A semantic view of classical proofs: type-theoretic, categorical, denotational characterizations.
In Proc. 11th IEEE Symp. Logic in Computer Science, New Jersey, July 1996, pages 230-241. IEEE Computer Society Press, 1996.

18

C.-H. L. Ong.
Observational equivalence of third-order Idealized Algol is decidable.
In Proceedings of IEEE Symposium on Logic in Computer Science, 22-25 July 200, Copenhagen Denmark, pages 245-256. Computer Society Press, 2002.

19

C.-H. L. Ong.
An approach to deciding observational equivalence of algol-like languages.
Unpublished preprint, 63 pages. To appear in Annals of Pure and Applied Logic, 2003.

20

C.-H. L. Ong and P. Di Gianantonio.
Games characterizing Levy-Longo trees.
Theoretical Computer Science, 312:121-142, 2004.

21

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, CSL'93, Swansea, UK, Sep. 1993, Selected Papers, pages 261-279, 1994.
LNCS Vol. 832.

22

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, Paris, January 1997, pages 215-227. ACM Press, 1997.

About this document ...

My Research

This document was generated using the LaTeX2HTML translator Version 99.1 release (March 30, 1999)

Copyright © 1993, 1994, 1995, 1996, Nikos Drakos, Computer Based Learning Unit, University of Leeds.
Copyright © 1997, 1998, 1999, Ross Moore, Mathematics Department, Macquarie University, Sydney.

The command line arguments were:
latex2html -split 0 summary

The translation was initiated by Luke Ong on 2004-04-05

Footnotes

... Collaboration¹

http://www.bell-labs.com/news/features/collaboration.html