🚀 go-pugleaf

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:

@InProceedings(Gordon85a,
	Copy=Y,
	Author="Mike Gordon",
	Title="Why Higher-Order Logic is a Good Formalisation for
	Specifying and Verifying Hardware",
	BookTitle=formasp,
	Editor="G Milne and P A Subrahmanyam",
	Publisher=nh,
	Address="Amsterdam",
	Pages="153--177",
	Year="1985")

A recent one is:

@InProceedings{Joyce91a,
  author = 	"Jeffrey J Joyce",
  title = 	"More Reasons Why Higher-Order Logic is a Good Formalism
		 for Specifying and Verifying Hardware",
  booktitle = 	miami,
  year = 	"1991",
  organization = 	"{ACM} {IFIP WG} 10.2",
  month = 	"January",
}

Kees
--
Kees Goossens                       Keep in Touch with the Dutch:
LFCS, Dept. of Computer Science     JANET: kgg@uk.ac.ed.lfcs
University of Edinburgh, Scotland   UUCP:  ..!mcsun!ukc!lfcs!kgg
Wiskunde is bouwen in de geest.	--- Luitzen Egbertus Jan Brouwer.

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