YUKQC@CUNYVM.BITNET (03/07/91)
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