🚀 go-pugleaf

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