🚀 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.