LICS Newsletter 46

Newsletter 48

November 19, 1997

[Past issues of the newsletter are available at 

  19-20 June, 1998 (just before LICS'98), Indianapolis, Indiana.
* Submission: An extended abstract (about 10-15 pages) should be mailed
  electronically to as PostScript, to be received 
  by March 15, 1998.  
* Topics of interest (non-exclusive) include modelling and
  verification of probabilistic and stochastic systems, including
  real-time and hybrid systems; formal models and verification
  techniques for randomized algorithms; semantics of probabilistic and
  stochastic processes; probabilistic and fuzzy logics; design of
  verification support tools; tool demonstrations; case studies. 
* Invited speakers: Rajeev Alur, Luca de Alfaro, Christel Baier, Vicky
  Hartonas-Garmhausen, Jeremy Gunawardena, Annabelle McIver, Prakash
  Panangaden, Roberto Segala, Scott Smolka, Moshe Vardi.
* Panel session: Ed Clarke, CMU, Panel Chair: What tools and theory
  are needed in order to make probabilistic verification practical?  
* Program committee: Marta Kwiatkowska (Chair),
  Michael Huth (Co-chair), plus invited speakers.
* Organizers: Marta Kwiatkowska, Michael Huth, Christel Baier and Mark

* Version 110 of Standard ML of New Jersey, a new release of the
  compiler conforming to the SML '97 revised definition, will be
  available during the week of November 25, 1997.  Information on how
  to obtain the new release SML/NJ can be found at the URL above.

  Call for participation
* The Program and Registration information for POPL '98 and FOOL 5
  (Foundations of Object-Oriented Languages) can be found at the URL
  above. This is the 25th POPL conference, and in honor of this
  anniversary there will be special invited talks by John Reynolds,
  Gerard Berry, and Mark Wegman, as well as a regular invited talk by
  Peter Lee. 

  Baltimore Convention Center, Baltimore, Maryland, January 9-10, 1998
  Call for participation
* All invited lectures and contributed paper sessions will be in
  (combined) Rooms 331 and 332 of the Baltimore Convention Center.
  Registration for the Joint Mathematical Meetings will be the Charles
  Street Lobby.  The meeting of the American Mathematical Society
  includes a special session on History of Mathematical Logic on
  Wednesday, January 7, in Room 322 of the Baltimore Convention
* Invited speakers. Juliet  Floyd, Marcia  Groszek, Joel  Hamkins,
  Dexter  Kozen, Isaac  Levi, Leonid  Libkin, Soren  Riis.
* Program committee. A. Carbone, M. Detlefsen, Y. Gurevich, A.
  Kanamori, L. Moss, and R. Parikh (Chair).

  August 22-28, 1998 Brno, Czech Republic
  Federated CSL/MFCS Conference
  Call for Papers
* CSL is the annual conference of the European Association for
  Computer Science Logic (EACSL).  The conference is intended for
  computer scientists whose research activities involve logic, as well
  as for logicians working on topics significant for computer
  science. In 1998 the CSL conference will be organized as a joint
  event with MFCS (Mathematical Foundations of Computer Science). The
  federated CSL/MFCS conference will have common plenary sessions and
  common social program. Participants registering for one conference
  can attend talks of both conferences.
* Invited talks.  Joint CSL/MFCS plenary talks: D. Harel, W. Maass,
  Y. Matiyasevic, M. Yannakakis.  CSL invited speakers: P. Hajek,
  J. Mitchell, I. Nemeti, Th. Schwentick, J. Tiuryn.  MFCS invited
  speakers: G. Ausiello, E. Boerger, Y. Gurevich, R. Karp,
  T. Leighton, K. Mehlhorn, M. Nielsen, A. Pnueli, P. Pudlak,
  C. Stirling.
* Submission.  Authors are invited to submit a draft or full paper (up
  to 12 pages). The cover page should include title, authors, and
  corresponding author (name, address, phone/fax number, e-mail
  address). Submission forms can be from the conference web page, or
  by sending an empty message with Subject: submission information to Deadline: April 15, 1998.
* Program co-chairs. G. Gottlob and E. Grandjean. 
* Program Committee: K. R. Apt, F. Baader, A. Carbone, T. Coquand,
  M. Fitting, A. Goerdt, M. Kanovich, C. Lautemann, A. Leitsch,
  D. Leivant, G. Longo, J. Paredaens, A. A. Razborov, A. Scedrov,
  K. Stroetmann, A. Voronkov.

  Call for papers
  Paris, France, April 27-28-29 1998
* Topics. Algorithms and architectures for "serial" and "on line"
  arithmetic.  Relations between number theory, automata theory and
  computer arithmetic.  Number systems. Floating point
  arithmetic. Calculability.  Symbolic manipulation of
  numbers. Algorithms for "exact" computing.  Multi-precision,
  interval arithmetic, stochastic arithmetic. Accuracy problems in
  various fields (geometry, physics, etc), and proposed solutions.
* Organization Committee. Jean-Marie Chesneaux, Fabienne Jezequel,
  Jean-Luc Lamotte, Jean Vignes.
* Program Committee.  Jean-Paul Allouche, Rene Alt, Jean-Claude
  Bajard, Jean-Claude Berges, Vasco Brattka, Jean-Marie Chesneaux,
  Martin Hotzel Escardo, Christiane Frougny, Peter Kornerup, David
  Lester, Pierre Liardet, Dominique Michelucci, Jean-Michel Muller,
  Nathalie Revol.
* Submissions.  Deadline: January 1, 1998.  You can submit a full
  paper (not an abstract) to Please request a pattern
  LaTeX file from the above URL address but send a postscript file. If
  you cannot use LaTeX, send 4 copies of a printed version to
  Jean-Marie Chesneaux, Laboratoire LIP6, Universite Pierre et Marie
  Curie, 4 place Jussieu, 75252 Paris Cedex 05, France. 

  Call for papers
  Hsi-tou, Taiwan, 16-19 June, 1998
* Invited speakers. David Beaver, Nick Chater, David Israel, Michiel
  van Lambalgen, Greg Mulhauser.
* Topics.  Foundations and applications of various approaches to the
  study of information, for example, Shannon-Weaver communication
  theory, Barwise-Seligman Channel theory, Situation Theory, Dynamic
  Semantics, Dretske's semantic theory of information.
  Information-based approaches to the syntax, semantics and pragmatics
  of natural language.  Information-based approaches to philosophy of
  mind, consciousness studies, and epistemology.
  Information-theoretic approaches to cognitive psychology.
  Information-theoretic approaches to induction and learning.
  Probabilistic methods in epistemology and logic.  Theory change,
  including Belief Revision and Bayesian approaches
* Submission.  Authors are invited to submit a detailed abstract of a
  full paper of at most 10 pages by e-mail to,
  using `ITALLC98 Submission' as the subject line.  The cover page
  should include title, authors and contact details of the
  corresponding author. Submission of postscript files is strongly
  encouraged.  The deadline for submissions is December 15, 1997.
* Program committee. Patrick Blackburn (Chair), Nick Braisby, Lawrence
  Cavedon, Sheila Glasbey, Atsushi Shimojima.

  November 4 - 6, 1998, Palo Alto, CA, USA
  Call for Papers
* Topics. Hardware verification techniques based on model checking,
  theorem proving, and related or hybrid methods. Correct by
  construction approaches to hardware design, such as synthesis and
  transformation. Hybrid approaches that integrate synthesis and
  verification or different verification techniques. Integration of
  formal methods with CAD tools, such as for synthesis, simulation,
  design exploration, and testing. Formalized reasoning techniques
  supporting hardware- and system-level description languages.  Case
  studies and application of formal methods in industry.
* Submission. 18-page, 12-point font (with abstract) for papers, and
  7-page, 12-point font abstract for tutorials and tool demos. Submit
  by April 20, 1998 via the FMCAD web-page
* Invited speakers. Ken McMillan, Carl Seger, Richard Platek, Amir
* Program committee. Ganesh Gopalakrishnan (co-chair), Phillip Windley
  (co-chair), Mark Aagaard, Randy Bryant, Jerry Burch, Albert
  Camilleri, Eduard Cerny, Shiu-Kai Chin, Ching-Tsun Chou, Francisco
  Corella, Limor Fix, Masahiro Fujita, Steve German, Tom Henzinger,
  Ramin Hojati, Alan Hu, Warren Hunt, Steve Johnson, Carlos Delgado
  Kloos, Thomas Kropf, Tim Leonard, Tom Melham, Carl Pixley, Mary
  Sheeran, Tom Shiple, Jens Skakkebaek (local arrangements), Mandayam
  Srivas, John Van Tassel, Ranga Vemuri.

* I am asking the Logic in Computer Science community for help in
  preparing a course on logic for computer science students at my
  school of engineering (at The Norwegian University of Science and
  Technology, Trondheim).  Your input consisting of a suggested
  curriculum, textbook and, especially, proposals of applications is
  most welcome. Pointers (http addresses) to existing courses are very
  appreciated.  The students will have taken propositional logic in
  the prerequiste course. Applications should be computer-based uses
  of logic showing logic at real work.  Our students are very good,
  the best in the country, but the teaching is (has been) mostly
  application oriented with little theory of computing training, if
  any. They will accept complex stuff provided the instructor can
  motivate them with good applications.
* Please send your replies by email:

  Goal-Directed Reasoning in Clausal Logic with Equality
  by M. Moser
  CS Press, Germany, 1997
  ISBN 3-931757-02-1
* The most successful approach for an efficient handling of equality
  is paramodulation restricted by orderings.  Unfortunately, this
  variant of paramodulation is only compatible with a bottom-up
  procedure where starting from a given set of clauses, new clauses
  are derived.  With respect to the crucial search space problem,
  however, goal-directed approaches have various advantages as they
  only allow inferences to be applied to the current goal.  Up to now,
  no practical solutions for the efficient handling of equality in a
  goal-directed setting have been found.  The topic of this book is an
  efficient approach for goal-directed and ordering-restricted
  reasoning in clausal logic with equality.  In order to attain
  completeness under these conditions, the goal-directed calculus
  needs to be combined with restricted bottom-up inference rules.  The
  completeness proof of the new calculus and its refinements is based
  on a new and powerful approach, covering different proof paradigms.
  Using this approach, it becomes possible to derive new correlations
  between the new calculus and other bottom-up and goal-directed

  The Action-as-Implication Paradigm 
  by B. Fronhoefer  
  CS Press, Germany, 1997
  ISBN 3-931757-91-9
* The Linear Connection Method is a restriction of the classical
  Connection Method for the purpose of plan generation.  Its basic
  idea is to formalize actions as implications.  The main part of the
  book deals with the logic underlying this approach.  The author
  shows that the mentioned restriction corresponds to a
  Horn-clause-like logic which is obtained through a restriction of
  the contraction rules in a suitable sequent system for classical
  logic.  On the way to this result a broad investigation yields
  matrix characterizations (in the sense of the Connection Method) of
  the multiplicative fragments of Contraction-Free Logic, Linear
  Logic, and Relevance Logic.  The method of investigation is by
  translation of sequent derivations into matrices and back.  For this
  purpose the Connection Method has been redeveloped for non-normal
  form matrices with multi-occurrences of literals and matrices are
  considered together with arbitrary sets of connections.  In the last
  chapter a proof search algorithm for the Linear Connection Method is
  presented, which is compared on benchmarks with the Situation
  Calculus and the planning system UCPOP.

  Postgraduate program "Specification of discrete processes
  and systems of processes by operational models and logics"
* Everbody who has a PhD degree in relevant areas, is invited to apply
  for this research grant. Please send your curriculum vitae including
  a list of publications to Prof. Dr.-Ing. habil. Heiko Vogler,
  Dresden University of Technology, Dept. of Computer Science, D-01062
  Dresden, Germany.
* Further information. See the URL above.

  August 17 - 21, 1998, Saarbrueken, Germany
  Call for papers
* Topics.  Philosophical foundations of probability, probabilistic
  logics, probabilistic proof systems, probabilistic proof checking,
  probabilistic knowledge representation, probabilistic games,
  randomised automata, randomised algorithms, semantics of
  probabilistic languages, probabilistic non-determinism,
  probabilistic reasoning, fuzzy and belief systems, inexact matching,
  constraints and probability, Markov Chain Monte Carlo Methods,
  practical applications, randomised optimisation (e.g. simulated
  annealing, genetic algorithms).
* Organisers.  Alessandra Di Pierro and Herbert Wiklicky.
* Submission.  Papers should be submitted in the form of an extended
  abstract of no more than 4000 words (8-10 pages) in length, and must
  include the e-mail address of all authors and a 200-300 word
  abstract.  Deadline is February 15, 1998.  To submit a paper, please
  send a postscript file to or
* Further information. See the URL above. 

  June 18th 1998, Marstrand, Sweden
  Call for papers
* Generic programming is about making programs more adaptable by
  making them more general. Generic programs often embody
  non-traditional kinds of polymorphism; ordinary programs are
  obtained from them by suitably instantiating their parameters.  In
  contrast with normal programs, the parameters of a generic programs
  are often quite rich in structure.  For example they may be other
  programs, types or type constructors, or even programming paradigms.
* The workshop will be on June 18th, 1998, directly following the
  Mathematics of Program Construction conference to be held in
  Marstrand Sweden.  We cordially invite all those with an active
  interest in this important new area to submit a short position paper
  on their work to one of the organizers.  Deadline for submission to
  the workshop is Feb. 16, 1997.
* Organizers. are as follows: Roland Backhouse (co-chair), Tim Sheard
  (co-chair), Johan Jeuring, Oege de Moor, Bernhard Moeller, Jose
  Oliveira, Barry Jay, Robin Cocket, Karl Lieberherr, Fritz Ruehr.