Path: utzoo!news-server.csri.toronto.edu!rutgers!usc!sdd.hp.com!uakari.primate.wisc.edu!samsung!uunet!mcsun!ukc!edcastle!cs.ed.ac.uk!kgg
From: kgg@cs.ed.ac.uk (Kees Goossens)
Newsgroups: comp.specification
Subject: Re: "higher-order" spec
Summary: Hardware Verification uses HOL
Message-ID: <7610@skye.cs.ed.ac.uk>
Date: 12 Mar 91 16:38:28 GMT
References: <91065.233041YUKQC@CUNYVM.BITNET>
Sender: nnews@cs.ed.ac.uk
Reply-To: kgg@lfcs.ed.ac.uk (Kees Goossens)
Organization: The Lavatory for the Foundations of Computer Science
Lines: 45

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.