LICS Newsletter 53

Newsletter 55

September 3, 1998

[Past issues of the newsletter are available at and]

LICS AND FLOC'99 MIRROR WEB SITES BOOK ANNOUNCEMENT Higher Order Operational Techniques in Semantics Edited by Andrew D. Gordon and Andrew M. Pitts Publications of the Newton Institute, Cambridge University Press, 390+viii pages. ISBN 0 521 63168 8. * Most object-oriented or functional languages are higher order languages, i.e., ones in which the means of manipulation, e.g., object or function, can itself be manipulated. This book contains a collection of original articles about recent developments in operational semantics for higher order programming languages by some of the leading researchers in the field. Operational techniques are important because they are closer to implementations and language definitions than more abstract mathematical techniques such as denotational semantics. One of the exciting developments reflected by the book is that mathematical structures and techniques used in denotational semantics (such as fixpoint induction) may be recovered from a purely operational starting point. The book surveys and introduces techniques such as contextual equivalence, applicative bisimulation, logical relations, improvement relations, explicit models of memory management, and labeling techniques for confluence properties. It treats a variety of higher order languages, based on functions, processes and objects, with and without side effects, typed and untyped. * Contents. Operational equivalences for untyped and polymorphic object calculi (A. D. Gordon), Semantics for core Concurrent ML using computation types (A. Jeffrey), Relational reasoning about contexts (S. B. Lassen), Labeling techniques and typed fixed-point operators (J. C. Mitchell, M. Hoang and B. T. Howard), Semantics of memory management for polymorphic languages (G. Morrisett and R. Harper), Operational reasoning for functions with local state (A. M. Pitts and I. D. B. Stark), Improvement theory and its applications (D. Sands), The coverage of operational semantics (S. F. Smith), Reasoning about functions with effects (C. Talcott). BOOK ANNOUNCEMENT The Incompleteness Phenomenon: A New Course in Mathematical Logic Second Edition Martin Goldstern and Haim Judah 1998, ISBN: 1-56881-093-8, paperback, 247pp., $39.00 To order, send email to: * The authors have written an introduction to logic taking Godel's incompleteness theorem as a starting point. The book should interest everyone from mathematicians to philosophers and readers who wish to understand the foundations and limitations of rational thinking. It is being used as a textbook at major colleges and universities but lends itself to self-study as well. * Table of Contents. 1. The Framework of Logic. 1.1 Induction. 1.2 Sentential Logic. 1.3 First Order Logic. 1.4 Proof Systems. 2. Completeness. 2.1 Enumerability. 2.2 The Completeness Theorem. 2.3 Nonstandard Models of Arithmetic. 3. Model Theory. 3.0 Introduction. 3.1 Elementary Substructures and Chains. 3.2 Ultraproducts and Compactness. 3.3 Types and Countable Models. 4. The Incompleteness Theorem. 4.0 Introduction. 4.1 The Language of Peano Arithmetic. 4.2 The Axioms of Peano Arithmetic. 4.3 Basic Theorems of Number Theory in PA. 4.4 Encoding Finite Sequences of Numbers. 4.5 Godel Numbers. 4.6 Substitution. 4.7 The Incompleteness Theorem. 4.8 Other Axiom Systems. 4.9 Bounded Formulas. 4.10 A Finer Analysis of 4.4 and 4.5. 4.11 More on Recursive Sets and Functions. BOOK ANNOUNCEMENT A = B Marko Petkovsek, Herbert Wilf and Doron Zeilberger Foreword by Donald E. Knuth 1996, ISBN: 1-56881-063-6, hardcover, 224pp., $39.00 To order, send email to: * This book shows how computers, using recently developed algorithms, can master the difficult job of simplifying complex summations and if there are no such simplifications they will prove this to be the case. The authors present the underlying mathematical theory of these methods, the principle theorems and proofs, and offer a package of computer programs on disk to carry out these tasks. The result is a story of very recent developments that have changed the field on which the game of discrete mathematics is played. BOOK ANNOUNCEMENT Erdos on Graphs: His Legacy of Unsolved Problems Fan Chung, Ron Graham 1998, ISBN: 1-56881-079-2, hardcover, 142pp., $30.00 To order, send email to: * This book is a tribute to Paul Erdos, the wandering mathematician once described as the prince of problem solvers and the absolute monarch of problem posers. It examines - within the context of his unique personality and lifestyle - the legacy of open problems he left to the world of mathematics after his death in 1996. Unwilling to succumb to the temptations of money and position, Erdos never had a home and never held a job. His home was a bag or two containing all his belongings and a record of the collective activities of the mathematical community. His job was one at which he excelled: identifying a fundamental roadblock in some particular line of research and capturing it in a well-chosen (often innocent-looking) problem, whose solution would likewise provide insight into the underlying theory. By cataloguing the unsolved problems of Erdos in a comprehensive and well-documented volume, the authors hope to continue the work of an unusual and special man who fundamentally influenced the field of mathematics. An appendix contains stories and reminiscences by one of Erdos' oldest friends and collaborators, Andy Vazsonyi. * Table of Contents. 1. Introduction. 2. Ramsey Theory. 3. Extremal Graph Theory. 4. Coloring, Packing, and Covering. 5. Random Graphs and Graph Enumeration. 6. Hypergraphs. 7. Infinite Graphs. 8. Erdos Stories As Told by Andy Vazsonyi. ANALYTIC TABLEAUX AND RELATED METHODS (TABLEAUX'99) June 7-11, 1999, Saratoga Springs, NY, USA Call for papers and tutorials * Topics, including (but not restricted to) analytic tableaux for various logics (theory and applications); related techniques and concepts, e.g., model checking and BDD's related methods (model elimination, sequent calculi, connection method, etc); new calculi and methods for theorem proving in classical and non-classical logics (modal, intuitionistic, linear, temporal, etc); systems, tools, implementations and applications (e.g., verification). * Submissions are invited in three categories: (A) Original research papers (up to 15 pages), (B) Original papers on system descriptions (up to 5 pages), (C) Tutorials in all areas of analytic tableaux and related methods from academic research to applications (proposals up to 5 pages). Authors are requested to submit via email in PostScript to the Program Chair ( by December 4, 1998. Submissions in categories A and B should preferably be in LaTeX2e llncs style. Please include, prepended in plain ascii, the names and e-mail addresses of authors, and the paper's title and abstract. * Program Chair: Neil V. Murray, Institute for Programming & Logics, Dept. of Computer Science LI-67A, University at Albany, Albany, NY 12222, USA, * Program Committee: P. Baumgartner, B. Beckert, K. Broda, R. Dyckhoff, A. Felty, C. Fermueller, M. Fitting, U. Furbach, D. Galmiche, R. Gore, J. Goubault-Larrecq, R. Haehnle, J. Hodas, C. Kreitz, R. Letz, D. Miller, U. Moscato, N. Murray, N. Olivetti, J. Pitt, E. Rosenthal, P. Schmitt, H. de Swart. FRONTIERS OF COMBINING SYSTEMS (FroCoS'98) October 2-4, 1998, University of Amsterdam, The Netherlands Call for Participation * See the above URL for further details. FOUNDATIONS OF SOFTWARE SCIENCE AND COMPUTATION STRUCTURES (FOSSACS'99) March 22-26, 1999, Amsterdam, the Netherlands Call for papers * Topics: FOSSACS seeks papers which offer progress in foundational research with a clear significance for software science. A central issue is theories and methods which support the specification, transformation, verification, and analysis of programs and software systems. Topics covered are: - Computational and syntactic foundations of software science: computation processes over discrete and continuous data, techniques for their manipulation, and their algorithmic, algebraic, and logical properties; - Transition systems, models of concurrency and reactive systems, and corresponding calculi, algebras, and logics; - Type theory, domain theory, and their connections to semantics of programming languages and software specification. * Submission: The deadline for receipt of submissions is 28 September 1998. Electronic submissions are strongly encouraged; details are found on the FOSSACS'99 Web page. Postal submissions should be sent to Prof. W. Thomas, RWTH Aachen, Informatik VII, D-52056 Aachen, Germany. Papers should be no more than 15 pages in the Springer-Verlag LNCS style. * Invited speaker: J. Esparza. * Program committee: R. di Cosmo, A.E. Emerson, J. Engelfriet, H. Ganzinger, D. Kozen, B. Jonsson, A. Jung, M. Nielsen, T. Nipkow, D. Niwinski, C.. Palamidessi, A. Petit, C. Stirling, W. Thomas. * FOSSACS'99 is a constituent of ETAPS'99, the European Joint Conferences on Theory and Practice of Software. For further details see THE FIRST INTERNATIONAL WORKSHOP ON LABELLED DEDUCTION (LD'98) September 7 - 9, 1998, Freiburg, Germany Call for participation * See the above URL for further details. VISITING LECTURER/PROFESSOR IN COMPUTER SCIENCE University of Technology at Darmstadt * There is a Visiting Lectureship/Professorship available at the University of Technology at Darmstadt for a period of either six months or one year starting on October 1, 1998. (There is an unexpected vacancy that occurred just yesterday.) In October we are starting a new curriculum 'Mathematics with Computer Science' with an international orientation. In the first year, courses are taught in English. There will be German and international students. The visiting Lecturer/Professor is expected to teach the first year course of Computer Science in English within this framework. The remuneration will be according to the German system depending on qualification and age. * Further information. Prof. Dr. Klaus Keimel, Fachbereich Mathematik, Technische Universitaet, D-64289 Darmstadt, Germany, Tel. + 49 6151 162215, Fax. + 49 6151 164011, e-mail: BRITISH LOGIC COLLOQUIUM September 21 - 22, King's College Cambridge Call for participation * The 1998 Meeting of the British Logic Colloqium September 21-22 1998, King's College Cambridge, UK. Talks at the meeting will cover a wide range of mathematical logic, philosophical logic and logic for computer science. The speakers are A. Dawar (Swansea), D. Evans (UEA), R. Gaskin (Sussex), J. Longley (Edinburgh), P Milne (Edinburgh), J. Paris (Manchester), M. Potter (Cambridge) and D. Pym (QMW, London). * Contact. Rosemarie Baines, King's College Research Centre, King's College, Cambridge CB3 7PX, UK; telephone: +44 (0)1223 331420; email: POSTDOCTORAL POSITION IN HARDWARE VERIFICATION Hardware Verification Group, Concordia University * The hardware verification research group at Concordia University in collaboration with researchers from University of Montreal and McGill University is looking forward to hiring a Postdoctoral Fellow to be involved in a 3-year research project entitled "Block-Based Design: Implementation-independent Descriptions and Tools for Design Verification and Synthesis". * The candidate should have a Ph.D. in Computer Science or Computer Engineering with experience in formal methods applied to design verification (hardware or software). Knowledge in digital hardware design is also desirable. The availability of the position is immediate, for the duration of max. 2 years. The salary is commensurate with experience, but limited by the granting NSERC agency at the maximum of 29 000$ CDN per year plus fringe benefits. * Send your CV by email as pure text, ps or pdf format to Prof. Sofiene Tahar, Dept. of Electrical and Computer Engineering, Concordia University, 1455 de Maisonneuve West - H961, Montreal, Quebec, H3G 1M8 Canada. * Further information. Visit the project web page. THE WORKSHOP ON COMPUTER SCIENCE AND INFORMATION TECHNOLOGIES (CSIT) January 18-22, 1999, Moscow, Russia * Topics. Data Theory and Logic, Theory of Programming, Theory of Computation, Distributed Computing and Communications, Concurrency and Parallelism, Mobile Computing Database Systems, Software and Data Engineering and CASE Methodology, Data Models, Data Mining, Data Warehousing, Internet and Databases, Persistent Systems, Heterogeneous and Federated Databases, Active Databases, Database Design, Object Oriented Databases, Mobile Databases, Engineering Databases, Temporal Databases, Multimedia Databases Query Languages, Query Processing, Query Optimization AI Methodologies, Expert Systems, Knowledge Engineering, WWW, Electronic Commerce Technologies, Digital Documents, Persistent Object Stores, Data Warehouse Design, OLAP Technology * Submission. Submit papers, as self-contained uuencoded gzipped Postscript, to before September 30, 1998. Submissions are limited to 12 A4-size pages, with 1 inch margins and 11 point or larger font. LECTURERS IN COMPUTER SCIENCE Queen Mary and Westfield College, London, UK * The Department is consolidating its research strength and seeking to appoint strong researchers in the areas of Distributed Systems, Human Computer Interaction, Computer Vision or Programming Languages and Theoretical Computer Science. Applicants with research interests in mobile computing, multimedia and CSCW are encouraged. At least one of the posts will be targeted at the areas of Distributed Systems or Human Computer Interaction. Candidates should be able to teach a range of undergraduate and postgraduate Computer Science courses. * Informal enquiries may be made to Professor Heather Liddell (Head of Department) on 0171 975 5167 - email: or Professor Peter Johnson on 0171 975 5224 - email: MATHEMATICAL FOUNDATIONS OF PROGRAMMING SEMANTICS (MFPS XV) Tulane University, New Orleans, April 28 - May 1, 1999 Call for Papers * The MFPS conferences are devoted to those areas of mathematics, logic and computer science which are related to the semantics of programming languages. The series particularly has stressed providing a forum where both mathematicians and computer scientists can meet and exchange ideas about problems of common interest. We also encourage participation by researchers in neighboring areas, since we strive to maintain breadth in the scope of the series. * Invited speakers. Martin Abadi, Matthew Hennessy, Tom Henzinger, Peter Selinger. * Special sessions. One will be on security, and is being organized by Martin Abadi, Catherine Meadows (NRL) and Dennis Volpano (Naval Postgraduate School). The second session will be on Object-Oriented Programming. * Program Committee Co-chairs. Andre Scedrov and Achim Jung. * Program Committee. Stephen Brookes, Adriana Compagnoni, Kathleen Fisher, Paul Gastin, Andrew Gordon, Reinhold Heckmann, Catherine Meadows, Michael Mislove, Peter O'Hearn, Catuscia Palamidessi, Prakash Panangaden, Dusko Pavlovic, Andrew Pitts, A. W. Roscoe, Giuseppe Rosolini, Jan Rutten, Eugene Stark. * Submissions. Submit extended abstracts of 12 pages or less. They should be in the form of a PostScript file that can print on any PostScript printer. Submissions either can be sent by email to or they can be deposited by anonymous ftp in the directory pub/incoming on the machine In the latter case, a message also should be sent to advising us of the submission. The deadline is November 3, 1998. * Further information. 4TH INTERNATIONAL CONFERENCE ON PRINCIPLES AND PRACTICE OF CONSTRAINT PROGRAMMING (CP98) Call for participation Pisa, Italy, October 26-30, 1998 * Invited Talks: -- Open Constraint Programming, Joxan Jaffar -- Heuristics for Constraint Satisfaction, Patrick Prosser -- Constructing Constraints, Peter Jeavons * Tutorials: -- Principles and Methods for Automated Reasoning: Variable Elimination versus Search, Rina Dechter -- Branch-and-infer: A unifying framework for integer linear programming and finite domain constraint programming, Alexander Bockmayr and Thomas Kasper -- Distributed Constraint Satisfaction: Foundation and Applications, Makoto Yokoo -- From Constraint Programming to Hybrid Problem-Solving Algorithms, Claude Le Pape and Mark Wallace * Satellite workshops: -- W1: Modeling and computing with Concurrent Constraint Programming -- W2: Large Scale Combinatorial Optimisation and Constraints -- W3: Constraint Problem Reformulation -- W4: Second Workshop on Constraints in Bioinformatics/Biocomputing -- W5: Set Constraints and Constraint-based Program Analysis * Details about the technical programme, and registration and accommodation information can be found at the concur98 web page. LIST OF RESEARCH GROUPS IN MATHEMATICAL LOGIC, PHILOSOPHICAL LOGIC AND THEORETICAL COMPUTER SCIENCE * A. Setzer has provided a list of research groups for mathematical logic, philosophical logic and theoretical computer science on the WWW, which contains links to related topics as well. See the above URL. CONFERENCE ON AUTOMATED DEDUCTION (CADE-16) July 7-10, 1999, Trento, Italy Call for papers * Topics. Logics of interest include propositional, first-order, equational, higher-order, classical, intuitionistic, constructive, nonstandard, and meta-logics, and type theory. Methods of interest include saturation, tableaux, term rewriting, induction, unification, constraint solving, decision procedures, model generation, model checking, logical frameworks, and AI-related methods for deductive systems such as proof planning and proof presentation. Applications of interest include hardware and software development, systems analysis and verification, deductive databases, functional and logic programming, computer mathematics, and deduction for natural language processing and other AI areas. Special topics of interest include proof theory, human-computer interfaces, distributed deduction, and search and simplification heuristics. * Paper Submission. Papers must be original and not submitted for publication elsewhere. Submission of a paper to more than one conference participating in FLoC is not permitted. Research papers can be up to 15 proceedings pages, and system descriptions can be up to 4 pages. Authors are strongly encouraged to use LaTeX2e and the Springer llncs class files available from the CADE-16 web site. The primary means of submission will be electronic, in PostScript format. Papers should be compressed, then uuencoded, then e-mailed to the program chair. Details on the procedure and alternatives can be found at the CADE-16 web site. Regardless of the submission method, the letter or e-mail message accompanying the paper must contain a plain text abstract of about 200 words and the names, e-mail addresses, and postal addresses of all authors. All submissions must be received by December 13, 1998. * Program Chair. Harald Ganzinger, Max-Planck-Institut fuer Informatik, Im Stadtwald, 66123 Saarbruecken, Germany, * Program Committee. F. Baader, L. Bachmair, D. Basin, A. Bundy, H. Comon, G. Dowek, H. Ganzinger, R. Hasegawa, J. Hsiang, D. Kapur, M. Kohlhase, H. Kirchner, A. Leitsch, R. Letz, P. Lincoln, C. Lynch, D. McAllester, W. McCune, R. Nieuwenhuis, H. de Nivelle, H. J. Ohlbach, L. Paulson, F. Pfenning, D. Plaisted, J. Slaney, T. Tammet, A. Voronkov, L. Wallen, D. Wang SYMPOSIUM ON THEORETICAL ASPECTS OF COMPUTER SCIENCE (STACS'99) March 4-6, Trier, Germany Call for papers * Topics. Algorithms and data structures, automata and formal languages, computational and structural complexity, semantics of programming languages,, theory of parallel and distributed computation, parallel algorithms, logic in computer science, algorithmic learning theory, computational geometry, cryptography, computer systems theory, program specification, verification, VLSI structures, theory of data bases, computational issues in artificial intelligence. * Submissions: Authors are invited to submit a draft of a full paper (5-12 pages). Electronic submission is highly recommended. Detailed information is available on the web site. Deadline for submission is September 11, 1998. * Program Committee. S. Albers, R. Amadio, R. Cori, J. Esparza, J. Hromkovic, C. Kenyon, J. Koebler, D. Krizanc, Ch. Meinel (chair), A. Petit, S. Rudich, J. Sgall, R. Silvestri, S. Tison, P. Widmayer.