The 16th FST&TCS Conference began with John Rushby's (SRI) invited talk, ``Mechanized formal methods: progress and prospects.'' He surveyed two historical paths: expressive specification languages, which were difficult to implement, and automated theorem proving, where systems were not expressive enough for programming applications. The arrival of model checking in the 1990s gave the ``horsepower'' required to find bugs in real systems. Rushby estimates Intel's overall loss on account of the infamous FDIV bug in the Pentium (including intangibles such as bad publicity), to be in the range of a billion US dollars. This has sent hardware manufacturers running for cover to the realm of mechanized formal methods.
The contributed papers were divided into parallel sessions, roughly corresponding to (A) algorithms and complexity, and (B) formal models of programs. In my view (and in retrospect), this was a bad decision, since it split up the Conference participants. One of the purposes of the Conference is to let people from all over India get to interact with and to know the work of their colleagues, and that may be getting diluted.
In the morning session on the B side, there were three papers on process algebras, dealing with bisimulation or testing preorders, as in Jain and Arun-Kumar's (IIT Delhi) paper.
Arvind's (MIT) talk in the afternoon was on ``A lambda calculus with letrecs and barriers,'' a technical subject which made many in the audience switch off.
In the following B side session, Tobias Nipkow (Tech Univ of Munich) gave an interesting account of mechanically checking the theorems in a textbook (Winskel's ``Formal Semantics of Programming Languages''). He succeeded in finding one bug in Winskel's book, and is now on to Hopcroft and Ullman's book on automata theory and formal languages.
On the second day of the meeting, J. Ian Munro (Waterloo) gave a comprehensive account of the problem of representing a subset of a large finite set (such as an index into the Oxford English Dictionary) in his invited talk ``Tables.''
In the B side session on papers in rewriting and logic, R. Ramanujam (IMSc) looked at a problem in temporal logic: can we decide whether a formula is ``inevitable,'' that is, whether for every system run, there is an interleaving of the run, which satisfies the formula? He showed that this is undecidable, but for an interesting subclass of ``coherent'' formulas, the problem remains decidable.
Knowledge-based programs allow the programmer to write ``if $p$ is known, do $S_1$ else do $S_2$.'' Ron van der Meyden (Univ of Tech, Sydney) looked for sufficient conditions for getting a finite-state implementation of such programs.
The afternoon of the second day had a special session in honour of the 60th birthday of Professor Rohit Parikh (City Univ of New York), chaired by R. Narasimhan (CMC Fellow). There were four invited talks, including two by Parikh's Ph.D. students Alessandra Carbone and Gilbert Ndjatou (Konstantinos Georgatos could not come), followed by a special talk by Parikh.
Vaughan Pratt (Stanford Univ), in his talk ``The logic of mathematics is linear,'' tried to persuade the audience that Chu spaces in ``universal'' topology form a basis for the foundations of mathematics. R. Ramanujam (IMSc) gave his new views on knowledge, which allow a resource-bounded reasoner to only look at a part of the system. Alessandra Carbone (Univ Paris XII) showed that short proofs of the existence of large numbers must necessarily involve proof-theoretic cycles. Gilbert Ndjatou (William Paterson College) is the first speaker at FST&TCS from Africa (Cameroon). He spoke on a propositional dynamic logic with a knowledge operator.
Rohit Parikh then gave a brief presentation of his ideas on ``Social software,'' the use of new protocols for societal interactions. As usual, his talk was laced with delightful examples, such as the one about the concurrency conference where all the participants were served coffee serially.
The third day began with Eric Allender's (Rutgers Univ) invited talk, entitled ``Circuit complexity before the dawn of the new millenium.'' He gave a personal, but well-motivated, sketch of recent developments in circuit complexity, leading to his recent work with Manindra Agrawal (IIT Kanpur) and S. Rudich which focuses attention on the question whether all NP-complete problems which are complete under poly-time reductions are complete under $NC^0$ reductions as well. This is true for all problems encountered in practice, but a proof that it is true for all problems would imply "P is not equal to NP".
In the final B side session, Milind Gandhe (Silicon Automation Systems) outlined his work with G. Venkatesh (SAS) and Amitabha Sanyal (IIT Bombay) on correcting terms which are ill-typed in the Curry system. Harald Sondergaard (Univ of Melbourne) presented a nice theorem on immediate fixpoints, and immediately applied it to analysis of groundedness in logic programs.
The University of Hyderabad has a sprawling campus well outside the city, and early in the mornings one could run into impromptu groups, heading for Mushroom Rock or Peacock Lake or just bird-watching. The organization, by a team under Arun Pujari, was excellent, in spite of the difficulties involved in transporting people staying in the city to and fro. The food was very good.
At the business meeting, R.K. Shyamasundar (TIFR), Vijay Chandru (IISc) and Somenath Biswas (IIT Kanpur) spoke on plans for IARCS activities in the coming year. The next FST & TCS will be held on 18-20 December 1997 in IIT Kharagpur, and the program co-chairs are G. Sivakumar and S. Ramesh (IIT Bombay).
The first session in ``Theory A'' began on time with N. Prabhu presenting their work on the d-step conjecture. Since the problem is accessible to almost everyone, the talk, though short on details, was interesting to everyone present. The feeling was that while the transformation suggested in the paper was interesting, there is still a lot of verifying to be done. The second talk was presented by S. Kapoor on approximating the Euclidean Travelling Salesman Problem. At the outset, he outlined how and where his work differed from S. Arora's work on the same. This paper proved lower bounds on the fast computability of $r$-times the optimal tour. The analysis hinged on the Minimum Spanning Tree construction. The third paper in the session was Rectilinear Geodesic Voronoi regions. This reviewer did not attend this paper.
The second session on Computational Geometry was on the same day, in the afternoon. S. Kapoor presented their work on the Dynamic Maintenance of Shortest Path trees in Polygons. The presentation was very competent but this reviewer was lost in a maze of ``funnels'' and ``chains''. I believe J. Gudmundsson presented their work on Rectangle Coverings of Polygons. The speaker spoke in a fairly accented english, but the pictures of sliding rectangles were fairly appealing. Finally P. Dasgupta spoki on Robots searching for loot in Caves. This made interesting viewing and the path for the robot suggested by the author had some nice continuities.
On the second day, in the morning session, B. Kalyanasundaram began with an analysis of Online Matchings of power stations to cities. The algorithm was fairly greedy and obvious, but the analysis was not. In the second talk R. M. Verma outlined a page replacement problem for multi-processing environments. The results were interesting but their version of limited look-ahead is debatable. N. Prabhu spoke enthusiastically on Quantum Mechanics and its applications to Optimization. Most of us were lost, besides the proceedings didn't help, since this material did not appear in the paper. The last speaker for the day was Prof. Oommen who spoke on syntactic pattern recognition. The problem was well presented and analysis was fairly combinatorial.
The Complexity Theory session was on the third day, in the morning. The authors of the first paper could not come due to unexpected problems with Indian visas, and their paper was presented by Eric Allender. The main result of the paper is an equivalence between deterministic CFLs and polynomial time Concurrent-Read-Owner-Write PRAMs, which generalizes to AuxPDAs with larger resource bounds. Rimli Sengupta presented their work on Non-cancellative Boolean circuits. This generalization of monotone circuits was introduced in a way which clearly brought out the motivations for studying such circuits, and some lower bounds and separations were presented. K. Lorys argued that efficient algorithms designed to run on QRQW PRAMs will overcome the impracticality of CRCW PRAMs and the difficulty of programming of EREW PRAMs; then went on to give lower bounds for QRQW PRAMs, evidence that these PRAMs are also not necessarily easy to program. Some of the analysis here semed very tedious and non-trivial. Manindra Agrawal ended the session with a host of results on restricted access to NP oracles through modular truth-table queries. He presented a game to assist the analysis, described some playing strategies, and manipulated all the audience's mind-changes through a master strategy that conclusively settled the odd question.