**Altenkirch, 1993**-
Altenkirch, T. (1993).
A formalization of the strong normalization proof for system F in
LEGO.
In [Bezem and Groote, 1993].
**Ben-Ari, 1984**-
Ben-Ari, M. (1984).
Algorithms for on-the-fly garbage collection.
*ACM Transactions on Programming Languages and Systems*, 6(3):333-344. **Bezem and Groote, 1993**-
Bezem, M. and Groote, J., editors (1993).
*International Conference on Typed Lambda Calculi and Applications*, volume 664 of*Lecture Notes in Computer Science*, March 16-18, 1993, Utrecht, The Netherlands. Springer. **Harper and Pollack, 1991**-
Harper, R. and Pollack, R. (1991).
Type checking with universes.
*Theoretical Computer Science*, 89:107-136. **Jones, 1992**-
Jones, C. (1992).
Completing the rationals and metric spaces in LEGO.
In Huet, G. and Plotkin, G., editors,
*Proceedings of the Second Annual Workshop on Logical Frameworks*. **Luo, 1994**-
Luo, Z. (1994).
*Computation and Reasoning: A Type Theory for Computer Science*. Oxford University Press. **Luo and Pollack, 1992**-
Luo, Z. and Pollack, R. (1992).
LEGO proof development system: User's manual.
Technical Report ECS-LFCS-92-211, Laboratory for Foundations of
Computer Science, University of Edinburgh.
**McKinna and Pollack, 1993**-
McKinna, J. and Pollack, R. (1993).
Pure type systems formalized.
In [Bezem and Groote, 1993].
**McKinna, 1992**-
McKinna, J. H. (1992).
*Delivarables: A Categorical Approach to Program Development in Type Theory*. PhD thesis, Laboratory for Foundations of Computer Science, University of Edinburgh.

Fri May 24 19:01:27 BST 1996