References

[1]

S.F. Allen, R.L. Constable, D.J. Howe and W.E. Aitken, `The Semantics of Reflected Proof', Proceedings of the 5th IEEE Symposium on Logic in Computer Science, pp. 95--105, 1990.

[2]

R.S. Boyer and J S. Moore, `Metafunctions: Proving Them Correct and Using Them Efficiently as New Proof Procedures', in: The Correctness Problem in Computer Science, edited by R.S. Boyer and J S. Moore, Academic Press, New York, 1981.

[3]

A.J. Camilleri, T.F. Melham and M.J.C. Gordon, `Hardware Verification using Higher-Order Logic', in: From HDL Descriptions to Guaranteed Correct Circuit Designs: Proceedings of the IFIP WG 10.2 Working Conference, Grenoble, September 1986, edited by D. Borrione (North-Holland, 1987), pp. 43--67.

[4]

M. Gordon, `Why higher-order Logic is a good formalism for specifying and verifying hardware', in: 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.

[5]

Donald. E. Knuth. The Art of Computer Programming. Volume 1/Fundamental Algorithms. Addison-Wesley, second edition, 1973.

[6]

Saunders Mac Lane and Garrett Birkhoff. Algebra. Collier-MacMillan Limited, London, 1967.

[7]

R. Milner, `A Theory of Type Polymorphism in Programming', Journal of Computer and System Sciences, Vol. 17 (1978), pp. 348--375.

[8]

George D. Mostow, Joseph H. Sampson, and Jean-Pierre Meyer. Fundamental Structures of Algebra. McGraw-Hill Book Company, 1963.

[9]

L. Paulson, `A Higher-Order Implementation of Rewriting', Science of Computer Programming, Vol. 3, (1983), pp. 119--149.

[10]

L. Paulson, Logic and Computation: Interactive Proof with Cambridge LCF, Cambridge Tracts in Theoretical Computer Science 2 (Cambridge University Press, 1987).

[11]

R.E. Weyhrauch, `Prolegomena to a theory of mechanized formal reasoning', Artificial Intelligence 3(1), 1980, pp. 133--170.

[12]

A.N. Whitehead and B. Russell, Principia Mathematica, 3 volumes (Cambridge University Press, 1910--3).