\begin{thebibliography}{}

\bibitem[Altenkirch, 1993]{altenkirch:strong}
Altenkirch, T. (1993).
\newblock A formalization of the strong normalization proof for system {F} in
  {\sc lego}.
\newblock In \cite{lncs664}.

\bibitem[Ben-Ari, 1984]{Benari:garbagecollection}
Ben-Ari, M. (1984).
\newblock Algorithms for on-the-fly garbage collection.
\newblock {\em ACM Transactions on Programming Languages and Systems},
  6(3):333--344.

\bibitem[Bezem and Groote, 1993]{lncs664}
Bezem, M. and Groote, J., editors (1993).
\newblock {\em International Conference on Typed Lambda Calculi and
  Applications}, volume 664 of {\em Lecture Notes in Computer Science}, March
  16-18, 1993, Utrecht, The Netherlands. Springer.

\bibitem[Harper and Pollack, 1991]{harper.pollack:universes}
Harper, R. and Pollack, R. (1991).
\newblock Type checking with universes.
\newblock {\em Theoretical Computer Science}, 89:107--136.

\bibitem[Jones, 1992]{jones:rationals}
Jones, C. (1992).
\newblock Completing the rationals and metric spaces in {\sc lego}.
\newblock In Huet, G. and Plotkin, G., editors, {\em Proceedings of the Second
  Annual Workshop on Logical Frameworks}.

\bibitem[Luo, 1994]{luo:typetheoryforcs}
Luo, Z. (1994).
\newblock {\em Computation and Reasoning: A Type Theory for Computer Science}.
\newblock Oxford University Press.

\bibitem[Luo and Pollack, 1992]{luo.pollack:legomanual}
Luo, Z. and Pollack, R. (1992).
\newblock {\sc Lego} proof development system: User's manual.
\newblock Technical Report ECS-LFCS-92-211, Laboratory for Foundations of
  Computer Science, University of Edinburgh.

\bibitem[McKinna and Pollack, 1993]{mckinna.pollack:pure}
McKinna, J. and Pollack, R. (1993).
\newblock Pure type systems formalized.
\newblock In \cite{lncs664}.

\bibitem[McKinna, 1992]{mckinna:phd}
McKinna, J.~H. (1992).
\newblock {\em Delivarables: A Categorical Approach to Program Development in
  Type Theory}.
\newblock PhD thesis, Laboratory for Foundations of Computer Science,
  University of Edinburgh.

\end{thebibliography}