Bibliography

• [Barwise77] BARWISE, Jon. Handbook of mathematical logic. North-Holland Publishing. 1977
• [Bertoni] BERTONI, A. MIGLIOLI P, Towards a Theory of Abstract Datya Types:  a discussion of problems and tools. International Symposium on Programming.  LNCS No. 83.  Springer-Verlag.
• [Cardoso93] CARDOSO, Rodrigo. Verificación y Desarrollo de Programas. Ediciones Uniandes. 1ra edición. 1993.
• [Goguen78]  GOGUEN, J.A. THATCHER J.W.  WAGNER E.G.  An initial approach to the specification, correctness, and implementation of abstract data types. 1978
• [Huet82]   HUET, Gérard.  HULLOT, Jean-Marie.  Proofs by induction in  equational theories    with constructors.  Journal of computer and system  science.  1982.
• [Kühler98] KÜHLER, Ulrich.  A Tactic-Based Inductive Theorem Prover for Data Types with    Partial Operations.  Doctoral Thesis.  University  Kaiserslautern.
• [Manna74] MANNA, Zohar.  Mathematical Theory of Computation. McGraw Hill Company. 1974
• [Meyer90] MEYER, Bertrand.  Introduction to the Theory of Programming Languages. Prentice Hall. 1990
• [O'Donell85] O'DONELL, Michael J.  Lecture Notes in Computer Science: Computing     in Systems Described by Equations. Springer-Verlag. 1977
• [O'Donell77] O'DONELL, Michael J.  Equational Logic as a Programming Language.

 The MIT Press. 1985
• [Toyama88] TOYAMA 88. Commutativity of term rewriting systems en Programming of future    generation Computers. North Holland.  1988

• [Leroy98] LEROY, Xavier. The Objective Caml system, documentation and user's guide.  Release 2.00. 1998
• [Leroy96] LEROY, Xavier. The Caml Light system Release 0.72. Documentation and user's manual. 1996