CALL FOR PARTICIPATION

          The 1991 International Tutorial and Workshop on the
            HOL Theorem Proving System and Its Applications

  Davis, California, USA                August 27 and August 28-30, 1991

The HOL system is a higher-order-logic theorem proving system implemented at
Cambridge University using methods developed at Edinburgh University.  It has
found many applications, from the verification of hardware designs at all
levels to the verification of programs and communication protocols.

This workshop is intended to bring together developers, users, potential users,
and others interested in the HOL theorem proving system to share information on
new development, extensions, and applications of HOL, and to discuss future
directions for improvements to HOL and its interfaces.

The 3-day workshop will be preceded by a full-day tutorial on August 27th,
consisting of presentations by a panel of invited HOL experts on a range of
topics including: an overview of the system; a survey of applications;
comparison of HOL with other interactive verification systems; what helps
and what hinders new users; the integration of HOL with existing methodologies,
tools and environments.  This tutorial is designed for an audience not
necessarily familiar with the HOL system or its applications; it is intended
primarily to give prospective users an informed basis for evaluating the HOL
system and its potential.

Papers are invited concerning new developments and extensions to HOL,
applications of HOL, including proof techniques, user interfaces for HOL and
interfaces between HOL and other systems, comparison of HOL with other
verification systems, and progress in other higher-order-logic proving systems.
Panel proposals on these topics also will be entertained.

Authors should send seven copies of a 1000 word abstract or panel proposal
to the HOL91 program coordinator, Phil Windley.  Electronic mail submissions in
PostScript format will also be accepted, for the convenience of European and
other overseas participants.  Abstracts or proposals must be received by
May 29, 1991.  Notification of acceptance will be made by July 1, 1991.  Papers
accepted for the workshop will be published in a Proceedings.

Non-authors are also encouraged to participate in the tutorial and/or workshop;
those wishing to attend should communicate with Myla Archer.  Travel
scholarships for amounts up to $1,000 may be available for full-time students,
awarded on a competitive basis.  For details, write to Jeff Joyce.

Co-sponsors:                        Keynote Speakers:

   IEEE Computer Society               Matt Kaufmann (Computational Logic Inc.)
   ACM SIGDA                           Kurt Keutzer (Synopsis Inc.)
   University of California, Davis     John Rushby (SRI International)
   University of Idaho
   University of British Columbia

Program Committee:

   Myla Archer  (University of California, Davis)
   Graham Birtwistle  (University of Calgary)
   Shui-Kai Chin  (Syracuse University)
   Luc Claesen  (IMEC / Kath. Univ. Leuven)
   Avra Cohn  (University of Cambridge)
   Michael Gordon  (University of Cambridge)
   Elsa Gunter  (AT&T Bell Labs)
   John Herbert  (University of Cambridge)
   Roger Jones  (ICL Defence Systems)
   Jeff Joyce  (University of British Columbia)
   Karl Levitt  (University of California, Davis)
   Paul Loewenstein  (Mitsubishi / Stanford University)
   Tom Melham  (University of Cambridge)
   Phil Windley  (University of Idaho)
   Glynn Winskel  (Aarhus University)

Organizing Committee:

   Myla Archer  (General Chair)         Karl Levitt  (Financial Chair)
    Division of Computer Science         Division of Computer Science
    University of California, Davis      University of California, Davis
    Davis, CA 95616, USA                 Davis, CA 95616, USA
    arc...@eecs.ucdavis.edu          lev...@eecs.ucdavis.edu
    (916) 752-7583                       (916) 752-0832
    fax: (916) 752-4767                  fax: (916) 752-4767

   Jeff Joyce  (Tutorials Chair)        Phil Windley  (Program Chair)
    Department of Computer Science       Department of Computer Science
    University of British Columbia       University of Idaho
    Vancouver, BC V6T 1W5, CANADA        Moscow, ID 83843, USA
    jo...@cs.ubc.ca                  wind...@cs.uidaho.edu
    (604) 228-4327                       (208) 885-6501
    fax: (604) 228-5485                  fax: (208) 885-6645

Local Arrangements Committee:

   Meshell Robinson (Chair)     robin...@cs.ucdavis.edu        (916) 752-1974
   George Fink                  gf...@cs.ucdavis.edu           (916) 752-8285
   Tom Schubert                 schub...@cs.ucdavis.edu        (916) 752-6452

Location and Accomodations:

   Davis is a small university town.  Its warm summer weather is conducive
   to recreational activities such as tennis, cycling and swimming.  Workshop
   participants will have access the extensive recreational facilities of
   the University.  Bicycles can be rented for rides to the country surrounding
   the Campus.  

   San Francisco is a 90 minute drive to the West and the northern Sierra
   Nevada Peaks are within 2 hours to the East.  Within 1 hour is the Napa
   Valley wine country.  

   A block of rooms at Davis motels within easy walking distance of the
   Campus have been reserved.  Details will be sent to registrants.

Doesn't this characterization of finiteness depend on some version of
the Axiom of Choice?  If memory serves, a set which fails to be finite
using this definition, includes an isomorphic copy of /omega.  However,
AC may fail so badly that there are Dedekind-finite, infinite sets: ones
which, while not equipotent to any natural number (viewed as the set of
all smaller ones), also fail to include an isomorphic copy of /omega
and so share the proposed property with the genuinely finite sets (ones
which are equipotent to some natural number.

However, we can do a little better.  Here is a characterization of
finiteness which DOES work (and is readily seen to be expressible in
2nd order logic):  a set X is finite iff X is well-orderable and all
well-orderings of X are order-isomorphic.

While Allan Adler is right of course, a direct appeal to the
compactness theorem may be more illuminating and not require the
machinery of ultraproducts:  Let T be any first order theory which has
(arbitrarily large) finite models, and let /THETA be any set of
sentences in any first order logic, with T /subset /THETA.  If /THETA
still has arbitrarily large finite models (e.g., iff MOD(/THETA) is the
class of all finite models of T), then /THETA also has an infinite
model by the compactness theorem, since by the compactness theorem,
letting /SIGMA be the set of all the /sigma_n, for n < /omega
(where /sigma_n is the sentence which asserts there are at least n
individuals), /THETA /union /SIGMA has a model (because every finite
subset does).
                                                           L.

Lee J. Stanley                     E-Mail:  L...@NS.CC.LEHIGH.EDU
Department of Mathematics                           or
Lehigh University                           L...@LEHIGH.BITNET
Bethlehem, PA, 18015

FAX:    215-758-3079              Phone:  215-758-3723
(please specify something                 VoiceMail after 4 rings!
 like: "Message for Lee                   starting Jan. 2, 1991
 Stanley, Math. Dept",
 at beginning of message)

In a footnote to his paper "Equality Between Functionals",  Harvey
Friedman mentions (without citing) the following result due to Gandy
and Kreisel:

There are two unequal primitive recursive functionals that agree on all
primitive recursive functional arguments.

In the above equality refers to equality in the full type hierarchy.
I would appreciate any references to the proof of this result.

Ramesh

Ramesh Subrahmanyam   |  Diplomat: A person who can tell you to go
Computer & Info. Sc.  |            to hell in such a way that you
U. of Pennsylvania    |            would look forward to the trip.

Philosophy & Computing

The journal is devoted to the use of computers and computational ideas
in both research and teaching in philosophy, applications of ideas from
philosophy in computing, and philosophical questions about the
foundations and impact of computers and computational ideas. Examples of
the first include the development of computer programs for the discovery
of scientific theories (philosophy of science), work on automated proof
construction (logic), work on case-based reasoning (ethical theory),
material on the use of text-analysis software (history of philosophy),
and the description and evaluation of innovative computer-assited
instructional materials. Examples of the second include the application
of speech act theory to computer programming languages or the
application of work on metaphor and analogy to natural language
understanding. Examples of the last include topics in computer ethics,
work on the nature of knowledge and expert systems, and discussions of
the possibility of artificial life.

Philosophy & Computing is the official journal of CAP. For information
about CAP contact: Robert Cavalier, CDEC Carnegie Mellon University,
Pittsburgh PA 15213-3890 USA; r...@andrew.cmu.edu; r...@andrew.bitnet.

Editor

Leslie Burkholder, Center for Design of Educational Computing, Carnegie
Mellon University

Editorial Board

Carl Bereiter, Centre for Applied Cognitive Science, Ontario Inst for
Studies in Education
T. W. Bynum, Research Center on Computing and Society, Southern
Connecticut State University
Preston Covey, CDEC and Dept of Philosophy, Carnegie Mellon University
Andre Fuhrmann, Zentrum Philosophie & Wissenschaftstheorie, Universitet
Konstanz
Peter Gardenfors, Cognitive Science, University of Lund
Peter Gibbins, Faculty of Mathematics, The Open University
Rod Girle, Automated Reasoning Project, Australian National University
Laurence Goldstein, Dept of Philosophy, University of Hong Kong
John Haugeland, Dept of Philosophy, University of Pittsburgh
Peter Millican, Dept of Philosophy, University of Leeds
James Moor, Dept of Philosophy, Dartmouth College
J F Pelletier, Luce Professor, Dept of Computer Science, University of
Rochester
John L Pollock, Dept of Philosophy, University of Arizona
William J. Rapaport, Dept of Computer Science and Center for Cognitive
Science, State University of New York at Buffalo
Stephen Read, Dept of Logic & Metaphysics, The University of St Andrews
Nicholas Rescher, Dept of Philosophy, University of Pittsburgh
Scott Roberts, The Annenberg/CPB Project
John Self, Dept of Computing, University of Lancaster
Roger C Schank, The Institute for the Learning Sciences, Northwestern
University
Wilfried Sieg, Dept of Philosophy, Carnegie Mellon University
Herbert Simon, Dept of Psychology, Carnegie Mellon University
Richard Spencer-Smith, AI Group, Middlesex Polytechnic
Paul Thagard, Cognitive Science Laboratory, Princeton University
Syun Tutiya, Dept of Philosophy, Chiba University

Subscription Enquiries
Ablex Publishing Corporation, 355 Chestnut Street, Norwood NJ 07648, USA

Advertising Enquiries and Other Business Correspondence
Ablex Publishing Corporation, 355 Chestnut Street, Norwood NJ 07648, USA

Information for Authors

The journal invites submissions on all topics within its scope.
Submissions should generally be in English. They should be addressed to
an audience of non-specialists. They may take the form of research or
tutorial or literature review articles, descriptions of innovative
software or its use and evaluation, and reviews of software and printed
materials.

Submissions may be made in either electronic or printed form. All
submissions should include an abstract. Electronic submissions may be
sent to the editor on disk or through email. Submissions on disk should
be either for MS-DOS or Macintosh. Printed submissions should be
double-spaced and include on a separate page the title, author's name,
and address. Submissions which include more than a few special symbols
or figures (for example, screen dumps) or more than a few instances of
special layout should be made in printed rather than electronic form.

All proposals, enquiries, and submissions should be sent to the editor:
Leslie Burkholder, CDEC Carnegie Mellon University, Pittsburgh PA
15213-3890; leslie.burkhol...@andrew.cmu.edu;
leslie.burkhol...@andrew.bitnet.

Authors of accepted submissions will be encouraged to submit electronic
copies of their submissions in addition to a final printed copy. One of
these electronic copies should be a stripped ASCII file of the text of
the article or review, with figures and tables in separate files. The
other should be a marked-up file (for example, a Microsoft Word file).
Notes should be endnotes rather than footnotes. References should follow
the American Psychological Association style guide; in particular,
references should be in the form "(<author surnames>, <date>, <pages>)"
and placed wherever possible in the text rather than a separate endnote.
Complete citations should be included in a bibliography.

Pleased (for my student) to say that my student found it, and pleased
to say (for Levy), that the hint given is just the right thing.
Use a bijection from V_/alpha /cross 2 to V_/alpha to simulate a flat
pairing function.  So, no need to reply.

                                                       L.

Lee J. Stanley                     E-Mail:  L...@NS.CC.LEHIGH.EDU
Department of Mathematics                           or
Lehigh University                           L...@LEHIGH.BITNET
Bethlehem, PA, 18015

FAX:    215-758-3079              Phone:  215-758-3723
(please specify something                 VoiceMail after 4 rings!
 like: "Message for Lee                   starting Jan. 2, 1991
 Stanley, Math. Dept",
 at beginning of message)