doc-src/Logics/logics.bbl

 \newblock North-Holland, 1980.
 
 \bibitem{alf}
 Lena Magnusson and Bengt {Nordstr\"om}.
 \newblock The {ALF} proof editor and its proof engine.
-\newblock In {\em Types for Proofs and Programs: International Workshop {TYPES
-  '93}}, LNCS 806, pages 213--237. Springer, published 1994.
+\newblock In Henk Barendregt and Tobias Nipkow, editors, {\em Types for Proofs
+  and Programs: International Workshop {TYPES '93}}, LNCS 806, pages 213--237.
+  Springer, published 1994.
 
 \bibitem{mw81}
 Zohar Manna and Richard Waldinger.
 \newblock Deductive synthesis of the unification algorithm.
 \newblock {\em Science of Computer Programming}, 1(1):5--48, 1981.
 
 \bibitem{martinlof84}
 Per Martin-L\"of.
 \newblock {\em Intuitionistic type theory}.
 \newblock Bibliopolis, 1984.
-
-\bibitem{melham89}
-Thomas~F. Melham.
-\newblock Automating recursive type definitions in higher order logic.
-\newblock In Graham Birtwistle and P.~A. Subrahmanyam, editors, {\em Current
-  Trends in Hardware Verification and Automated Theorem Proving}, pages
-  341--386. Springer, 1989.
 
 \bibitem{milner-coind}
 Robin Milner and Mads Tofte.
 \newblock Co-induction in relational semantics.
 \newblock {\em Theoretical Computer Science}, 87:209--220, 1991.

   Tallinn, Published 1990. Estonian Academy of Sciences, Springer.
 
 \bibitem{paulson-final}
 Lawrence~C. Paulson.
 \newblock A concrete final coalgebra theorem for {ZF} set theory.
-\newblock In {\em Types for Proofs and Programs: International Workshop {TYPES
-  '94}}, LNCS 996, pages 120--139. Springer, published 1995.
+\newblock In Peter Dybjer, Bengt Nordstr{\"om}, and Jan Smith, editors, {\em
+  Types for Proofs and Programs: International Workshop {TYPES '94}}, LNCS 996,
+  pages 120--139. Springer, published 1995.
 
 \bibitem{pelletier86}
 F.~J. Pelletier.
 \newblock Seventy-five problems for testing automatic theorem provers.
 \newblock {\em Journal of Automated Reasoning}, 2:191--216, 1986.