9. REFERENCES

 [Atk85]   Atkinson, Malcolm P,; Morrison, Ronald: Types, Bindings and
           Parameters in a Persistent Environment.  In: Persistent and
           Data Types, Persistent Programming Research Report 16,
           University of Glasgow, 1985

 [Boy81]   Boyer, RS,; Moore, J,S,: Metafunctions: proving them correct
           and using them efficiently as new proof procedures.  In "The
           Correctness Problem in Computer Science" (R.S.Boyer and
           J.S.Moore, eds.), Academic Press, New York 1981.

 [Bur84]   Burstall, R.; Lampson, B.: A Kernel Language for Abstract
           Data Types and Modules, Proc. Int. Symp. on Semantics of Data
           Types, 1984.

 [Con80]   Constable, R.L.: Programs and Types. Proceedings of the 21st
           Annual Symposium on Foundations of Computer Science,
           Syracuse, N.Y. 1980.

 [Cur72]   Curry, H.B.; Hindley, J.R.; Seldin, J.P.: Combinatory Logic
           Volume II.  North Holland Publishing Company, 1972.

 [God31]   Godel, Kurt: On Completeness and Consistency. In [Hei67].

 [Gor79]   Gordon, M.; Milner, R.; Wadsworth, C,: Edinburgh LCF.
           Springer-Verlag, Lecture Notes in Computer Science, Vol. 78.

 [Hat82]   Hatcher, William S,: The Logical Foundations of Mathematics.
           Pergamon Press 1982.

 [Hei67]   van Heijenoort, Jean: From Frege to Godel, a sourcebook in
           Mathematical Logic, 1879-1931.
           Harvard University Press, 1967.

 [Hin72]   Hindley, J.R,; Lercher, B.; Seldin, J.P.: Introduction to
           Combinatory Logic.  Cambridge University Press, 1972.

 [Joh84]   Johnsson, Thomas: Efficient Compilation of Lazy Evaluation.
           SIGPLAN Notices Vol.19, No. 6, June 1984.

 [Lam80]   Lambek, J.: From lambda-calculus to Cartesian Closed
           Categories.    In: To H,B.Curry: Essays on Combinatory Logic,
           Lambda-calculus and Formalism.        Edited by J.P.Seldin and
           J.R.Hindley. Academic Press 1980.

 [Mar75]   Martin-Lof P,: An intuitionistic theory of types: predicative
           part, In Logic Colloquium 173, pp 73-118, North Holland 1975.

 [Mar82]   Martin-Lof, Per: Constructive Mathematics and Computer
           Programming, In Logic, Methodology and Philosophy of Science,
           VI (Proc. of the 6th Int.  Cong., Hanover, 1979).  North
           Holland Publishing Company, Amsterdam (1982).

 [Nik85]   Nikhil, R.S.:   Functional Databases, Functional Languages,
           In: Persistent and Data Types, Persistent Programming
           Research Report 16, University of Glasgow, 1985.

 [Nip85]   Nipkow, T,N,:    Mule: Persistence and Types in an IPSE. In:
           Persistent and Data Types, Persistent Programming Research
           Report 16.  University of Glasgow, 1985.

 [Qui63]   Quine, W,V,O,: Set Theory and its Logic. Harvard University
           Press, 1963.

 [Rus03]   Russell, B,: The Principles of Mathematics. George Allen &
           Unwin Ltd., 1903.

 [Rus08]   Russell, B,:    Mathematical Logic as based on the Theory of
           Types.  American journal of Mathematics 30, 222-262.  Also in
           [Hei67].

 [Sco70]   Scott, Dana: Outline of a Mathematical Theory of Computation,
           oxford University Computing Laboratory, PRG-2.  Nov 1970,

 [Tur79a]  Turner, D.A.: Another Algorithm for Bracket Abstraction.
           Journal of Symbolic Logic, Vol. 44, No. 2, June 1979.

 [Tur79b]  Turner, D.A.: A new implementation technique for applicative
           languages.  Software - Practice and Experience, Vol. 9. 31-49
           (1979)

 [Tur84]   Turner, D.A.: Functional programs as executable
           specifications.   Phil. Trans. R. Soc. Lond. A 312, 363-388
           (1984).

© dated 86/7/15 HTML 96/6/6 edited 96/6/15