1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
|
\begin{thebibliography}{99}
\bibitem{Nuprl} % OK
S.F.\ Allen, R.L.\ Constable, D.J.\ Howe and W.E. Aitken,
`The Semantics of Reflected Proof',
{\it Proceedings of the 5th IEEE Symposium on Logic in Computer Science\/},
pp.\ 95--105, 1990.
\bibitem{BoyerMoore} % OK
R.S.\ Boyer and J\ S.\ Moore, `Metafunctions: Proving Them Correct and
Using Them Efficiently as New Proof Procedures', in: {\it The
Correctness Problem in Computer Science}, edited by
R.S.\ Boyer and J\ S.\ Moore, Academic Press, New York, 1981.
\bibitem{Camilleri-et-al} % OK
A.J.\ Camilleri, T.F.\ Melham and M.J.C. Gordon,
`Hardware Verification using Higher-Order Logic',
in: {\it From HDL Descriptions to Guaranteed Correct \mbox{Circuit}
Designs: Proceedings of the IFIP WG 10.2 Working Conference, Grenoble,
September 1986}, edited by D.\ Borrione (North-Holland, 1987), pp.\ 43--67.
\bibitem{Why-HOL-paper} % OK
M.\ Gordon,
`Why higher-order Logic
is a good formalism for specifying and verifying hardware',
in: {\it Formal Aspects of VLSI Design: Proceedings of the 1985 Edinburgh
Workshop on VLSI\/}, edited by G.\ Milne and
P.A.\ Subrahmanyam (North-Holland, 1986), pp.\ 153--177.
\bibitem{knuth73} % OK
Donald.\ E. Knuth.
{\em The Art of Computer Programming}. Volume 1/Fundamental
Algorithms. Addison-Wesley, second edition, 1973.
\bibitem{maclane67}
Saunders\ Mac Lane and Garrett Birkhoff. {\em Algebra}.
Collier-MacMillan Limited, London, 1967.
\bibitem{Milner-types} % OK
R. Milner,
`A Theory of Type Polymorphism in Programming',
{\it Journal of Computer and System Sciences}, Vol.\ 17 (1978),
pp.\ 348--375.
\bibitem{mostow63} % OK
George\ D. Mostow, Joseph\ H. Sampson, and Jean-Pierre Meyer.
{\em Fundamental Structures of Algebra}. McGraw-Hill Book Company, 1963.
\bibitem{lcp_rewrite} % OK
L.\ Paulson,
`A Higher-Order Implementation of Rewriting',
{\it Science of Computer Programming}, Vol.\ 3, (1983), pp.\ 119--149.
\bibitem{new-LCF-man} % OK
L.\ Paulson,
{\it Logic and Computation: Interactive Proof with Cambridge LCF},
Cambridge Tracts in Theoretical Computer Science 2
(Cambridge University Press, 1987).
\bibitem{FOL} % OK
R.E.\ Weyhrauch, `Prolegomena to a theory of mechanized formal reasoning',
{\it Artificial Intelligence\/} {\bf 3(1)}, 1980, pp.\ 133--170.
\bibitem{Principia} % OK
A.N.\ Whitehead and B.\ Russell,
{\it Principia Mathematica},
3 volumes (Cambridge University Press, 1910--3).
\end{thebibliography}
|
