next up previous contents
Next: About this document Up: The LEGO library Previous: Other work


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