References

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.