Path: utzoo!utgpu!news-server.csri.toronto.edu!rpi!usc!snorkelwacker.mit.edu!bloom-beacon!eru!kth.se!sunic!mcsun!ukc!cam-cl!news
From: sk@ely.cl.cam.ac.uk (Sara Kalvala)
Newsgroups: comp.specification
Subject: Re: "higher-order" spec
Message-ID: <1991Mar20.100608.19267@cl.cam.ac.uk>
Date: 20 Mar 91 10:06:08 GMT
References: <91065.233041YUKQC@CUNYVM.BITNET> <7610@skye.cs.ed.ac.uk>
Sender: news@cl.cam.ac.uk (The news facility)
Reply-To: sk@cl.cam.ac.uk
Organization: Cambridge Hardware Verification Group
Lines: 40

In article <7610@skye.cs.ed.ac.uk>, kgg@cs.ed.ac.uk (Kees Goossens) writes:
|> In article <91065.233041YUKQC@CUNYVM.BITNET> YUKQC@CUNYVM.BITNET writes:
|> >
|> >I am looking for articles that contain
|> >concrete examples of formal specification in "higher-order
|> >formalisms". By "higher-order formalisms", I intend any formal calculus
|> >about higher-order objects of any sort, say, higher-order predicate
|> >calculus, Church's Simple Theory of Types, higher-order type theories,
|> >set theories, etc.
|> >
|> > ...
|> 
|> Hardware verification uses a lot of higher order logic (classical,
|> constructive, partial terms, polymorphic etc), type theory etc.
|> There are masses of articles on this topic. The classic is:


More examples of the use of HOL (Higher Order Logic) for specification are
included in the documentation for the HOL system, which contains in the
tutorial section:

	- A sliding window protocol, by Rachel Cardell-Oliver.
	- A simple microprocessor system, Jeff Joyce.
	- Modular arithmetic, by Elsa Gunther.

The documentation is being prepared by SRI Cambridge and DSTO Australia.
LaTeX sources (as well as the sources for the HOL system) are available by
contacting me; the final printed version will be available in a few months
from SRI Cambridge. I don't believe the tutorial section is going to be
changed much.


						- Sara Kalvala
						sk@cl.cam.ac.uk

						University of Cambridge
						Computer Laboratory
						New Museums Site
						Pembroke Street
						Cambridge CB2 3QG, ENGLAND