Preview
Unable to display preview. Download preview PDF.
References
Anthony Bailey. Representing algebra in LEGO. Master's thesis, University of Edinburgh, 1993.
Henk Barendregt. Introduction to Generalised Type Sytems. J. Functional Programming, 1(2):125–154, April 1991.
Henk Barendregt. Lambda calculi with types. In Abramsky, Gabbai, and Maibaum, editors, Handbook of Logic in Computer Science, volume II. Oxford University Press, 1992.
Stefano Berardi. Type Dependence and Constructive Mathematics. PhD thesis, Dipartimento di Informatica, Torino, Italy, 1990.
Robert L. Constable, et. al. Implementing Mathematics with the Nuprl Proof Development System. Prentice-Hall, Englewood Cliffs, NJ, 1986.
Gilles Dowek and Robert Boyer. Towards checking proof checkers. In Herman Geuvers, editor, Informal Proceedings of the Nijmegen Workshop on Types for Proofs and Programs, May 1993.
Dowek, Felty, Herbelin, Huet, Murthy, Parent, Paulin-Mohring, and Werner. The Coq proof assistant user's guide, version 5.8. Technical report, INRIA-Rocquencourt, February 1993.
Herman Geuvers. Logics and Type Systems. PhD thesis, Department of Mathematics and Computer Science, University of Nijmegen, 1993.
Herman Geuvers and Mark-Jan Nederhof. A modular proof of strong normalization for the calculus of constructions. Journal of Functional Programming, 1(2):155–189, April 1991.
Robert Harper and Robert Pollack. Type checking with universes. Theoretical Computer Science, 89:107–136, 1991.
Gérard Huet. The constructive engine. In R. Narasimhan, editor, A Perspective in Theoretical Computer Science. World Scientific Publishing, 1989. Commemorative Volume for Gift Siromoney.
Claire Jones and Randy Pollack. Incremental changes in LEGO: 1993. Available by anonymous ftp with LEGO distribution, May 1993.
Claire Jones and Randy Pollack. Incremental changes in LEGO: 1994. Available by anonymous ftp with LEGO distribution, May 1994.
Zhaohui Luo and Robert Pollack. LEGO proof development system: User's manual. Technical Report ECS-LFCS-92-211, LFCS, Computer Science Dept., University of Edinburgh, The King's Buildings, Edinburgh EH9 3JZ, May 1992. Updated version. Available by anonymous ftp with LEGO distribution.
Z. Luo. Computation and Reasoning: A Type Theory for Computer Science. International Series of Monographs on Computer Science. Oxford University Press, 1994.
James McKinna. Typed λ-calculus formalized: Church-Rosser and standardisation theorems. In preparation, 1994.
James McKinna and Robert Pollack. Pure Type Sytems formalized. In M. Bezem and J.F. Groote, editors, Proceedings of the International Conference on Typed Lambda Calculi and Applications, TLCA'93, pages 289–305. Springer-Verlag, LNCS 664, March 1993.
Gopalan Nadathur and Debra Sue Wilson. A notation for lambda terms I: A generalization of environments. Technical Report Technical Report CS-1993-22, Duke University, 1993.
R. Pollack. Typechecking in Pure Type Sytems. In Informal Proceedings of the 1992 Workshop on Types for Proofs and Programs, Båstad, Sweden, pages 271–288, June 1992. Available by ftp.
Robert Pollack. The Theory of LEGO: A Proof Checker for the Extended Calculus of Constructions. PhD thesis, University of Edinburgh, 1994. Available by anonymous ftp from ftp.cs.chalmers.se in directory pub/users/pollack.
L.S. van Benthem Jutting. Typing in Pure Type Sytems. Information and Computation, 105(1):30–41, July 1993.
L.S. van Benthem Jutting, James McKinna, and Robert Pollack. Checking algorithms for Pure Type Systems. In Henk Barendregt and Tobias Nipkow, editors, Types for Proofs and Programs: International Workshop TYPES'93, Nijmegen, May 1993, Volume 806 of LNCS, pages 19–61. Springer-Verlag, 1994.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1995 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Pollack, R. (1995). A verified typechecker. In: Dezani-Ciancaglini, M., Plotkin, G. (eds) Typed Lambda Calculi and Applications. TLCA 1995. Lecture Notes in Computer Science, vol 902. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0014065
Download citation
DOI: https://doi.org/10.1007/BFb0014065
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-59048-4
Online ISBN: 978-3-540-49178-1
eBook Packages: Springer Book Archive