kgg@cs.ed.ac.uk (Kees Goossens) (03/13/91)
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.
sk@ely.cl.cam.ac.uk (Sara Kalvala) (03/20/91)
In article <7610@skye.cs.ed.ac.uk>, kgg@cs.ed.ac.uk (Kees Goossens) writes: |> 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: More examples of the use of HOL (Higher Order Logic) for specification are included in the documentation for the HOL system, which contains in the tutorial section: - A sliding window protocol, by Rachel Cardell-Oliver. - A simple microprocessor system, Jeff Joyce. - Modular arithmetic, by Elsa Gunther. The documentation is being prepared by SRI Cambridge and DSTO Australia. LaTeX sources (as well as the sources for the HOL system) are available by contacting me; the final printed version will be available in a few months from SRI Cambridge. I don't believe the tutorial section is going to be changed much. - Sara Kalvala sk@cl.cam.ac.uk University of Cambridge Computer Laboratory New Museums Site Pembroke Street Cambridge CB2 3QG, ENGLAND