Path: utzoo!utgpu!news-server.csri.toronto.edu!cs.utexas.edu!sdd.hp.com!wuarchive!psuvax1!psuvm!cunyvm!yukqc
From: YUKQC@CUNYVM.BITNET
Newsgroups: comp.specification
Subject: "higher-order" spec\
Message-ID: <91065.233041YUKQC@CUNYVM.BITNET>
Date: 7 Mar 91 04:30:41 GMT
Organization: City University of New York/ University Computer Center
Lines: 29


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.

More specifically, what I am really interested in is an article that

(1) illustrates the use of a higher-order formalism by concrete examples
    of specification; or
(2) advances some arguments about the advantages/disadvantages of higher-order
    formalisms in formal specification from various viewpoints, e.g.,
    expressive power, ease of composing specification,
    understandability, integration with program verification/synthesis
    systems, etc.

Of course, I'd be happy to hear your opinion as to whether
"higher-orderedness" is really good or bad, even if you've never published
it! I'll post a summary of replies if I get more than a couple.


Thanks in advance.

Keitaro Yukawa
Dept. of Computer Science
Queens College
City University of New York