Return-Path: <John.Harrison-request@cl.cam.ac.uk>
Delivery-Date: 
Received: from leopard.cs.byu.edu (no rfc931) by swan.cl.cam.ac.uk 
          with SMTP (PP-6.5) outside ac.uk; Tue, 19 Oct 1993 16:17:59 +0100
Received: by leopard.cs.byu.edu (1.37.109.4/16.2) id AA24122;
          Tue, 19 Oct 93 09:06:28 -0600
Sender: info-hol-request@leopard.cs.byu.edu
Errors-To: info-hol-request@leopard.cs.byu.edu
Precedence: bulk
Received: from dworshak.cs.uidaho.edu by leopard.cs.byu.edu 
          with SMTP (1.37.109.4/16.2) id AA24118; Tue, 19 Oct 93 09:06:20 -0600
Received: from swan.cl.cam.ac.uk by dworshak.cs.uidaho.edu 
          with SMTP (1.37.109.4/16.2) id AA25879; Tue, 19 Oct 93 08:05:51 -0700
Received: from auk.cl.cam.ac.uk (user jg (rfc931)) by swan.cl.cam.ac.uk 
          with SMTP (PP-6.5) to cl; Tue, 19 Oct 1993 16:03:29 +0100
To: info-hol@cs.uidaho.edu
Subject: Re: Theorem provers of the world
In-Reply-To: Your message of "Mon, 18 Oct 93 10:15:19 BST." <"swan.cl.cam.:130670:931018091558"@cl.cam.ac.uk>
Date: Tue, 19 Oct 93 16:03:24 +0100
From: Jim Grundy <Jim.Grundy@cl.cam.ac.uk>
Message-Id: <"swan.cl.cam.:201710:931019150332"@cl.cam.ac.uk>


Well, I have the following:

(That is I have these references - I have not actually seen some of them)

@BOOK{Ble84a,
    editor      = "W. W. Bledsoe and D. W. Loveland",
    title       = "Automated Theorem Proving: After 25 Years",
    publisher   = "American Mathematical Society",
    year        = 1984}

@ARTICLE{Che81,
    author      = "M. H. Cheheyl and M. Gasser and G. A. Huff and J. K. Millen",
    title       = "Verifying Security",
    journal     = "Computer Surveys",
    year        = 1981,
    volume      = 13,
    pages       = "279--339"}

@TECHREPORT{Cra81,
    author      = "Dan Craigen",
    title       = "Formal Verification of Programs:
                    Summary, Conclusions and Recomendations",
    institution = "I. P. Sharp \& Associates",
    address     = "Ottawa, Canada",
    year        = 1981,
    number      = 5,
    type        = "Technical Report"}

@TECHREPORT{Cra85,
    author      = "Dan Craigen",
    title       = "A Technical Review of Four Verification Systems:
                    Gypsy, Affirm, FDM and Revised Special",
    institution = "I. P. Sharp \& Associates",
    address     = "Ottawa, Canada",
    year        = 1985,
    type        = "Technical Report"}

@TECHREPORT{Kau87,
    author      = "M. Kaufmann and W. D. Young",
    title       = "Comparing Gypsy and the Boyer Moore Logic for
                    Specifying Secure Systems",
    institution = "Institute for Computer Science and Computer Applications,
                    University of Texas at Austin",
    address     = "Austin, Texas, United States",
    year        = 1987,
    number      = 59,
    type        = "Technical Report"}

@TECHREPORT{Lin86a,
    author      = "Peter A. Lindsay and Richard C. Moore and Brian Ritchie",
    title       = "Review of Existing Theorem Provers",
    institution = "Department of Computer Science, University of Manchester",
    address     = "Manchester M12~9PL, England",
    year        = 1986,
    month       = "December",
    number      = "UMCS-87-8-2"}

@ARTICLE{Lin88a,
    author      = "Peter A. Lindsay",
    title       = "A Survery of Mechanical Support for Formal Reasoning",
    journal     = "Software Engineering Journal",
    year        = 1988,
    month       = "January"
    pages       = "3--27"}

@TECHREPORT{Sam90,
    author      = "A. Sampaio",
    title       = "A Comparitive Study of Theorem Provers:
                    proving correctness of compiling specifications",
    institution = "Oxford University, Computing Laboratory,
                    Programming Research Group",
    address     = "8--11 Keble Road, Oxford\ \ OX1 3QD, England",
    year        = 1990,
    number      = "PRG-TR-20-90",
    type        = "Technical Report"}

@TECHREPORT{Smi90a,
    author      = "Alf Smith",
    title       = "Which Theorem Prover? (A Survey of Four Theorem Provers)",
    institution = "Royal Signals and Radar Establishment",
    address     = "St Andrews Road, Malvern, Worcestershire WR14~3PS, England",
    year        = 1990,
    month       = "Octover"
    number      = 4430,
    type        = "Memorandum"}

@INBOOK{Sup84,
    author      = "P. Suppes",
    title       = "The Next Generation of Interactive Theorem Provers"
    series      = "Lecture Notes in Computer Science",
    volume      = 170,
    publisher   = "Springer-Verlag",
    address     = "Berlin, Germany",
    year        = 1984,
    pages       = "303--315"}

@INPROCEEDINGS{You89a,
    author      = "William D. Young",
    title       = "Comparing Specification Paradigms: {G}ypsy and {Z}",
    booktitle   = "Proceedings of the\
                    12th National Computer Security Conference",
    year        = 1989,
    month       = "October"
    pages       = "83--97"}

Jim

===============================================================================
Jim Grundy               
University of Cambridge | Phone: +44 223 334729            | This space has
Computer Laboratory     | Fax:   +44 223 334678            | been intentionally
New Museums Site        | Telex: CAMSPLG 81240             | left blank for
Pembroke Street         | email: Jim.Grundy@cl.cam.ac.uk   | formatting
Cambridge  CB2 3QG      |                                  | purposes.
UNITED KINGDOM          |                                  |
===============================================================================