{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,9]],"date-time":"2026-05-09T02:42:01Z","timestamp":1778294521015,"version":"3.51.4"},"publisher-location":"Berlin\/Heidelberg","reference-count":16,"publisher":"Springer-Verlag","isbn-type":[{"value":"3540565175","type":"print"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/bfb0037113","type":"book-chapter","created":{"date-parts":[[2006,1,25]],"date-time":"2006-01-25T15:21:36Z","timestamp":1138202496000},"page":"289-305","source":"Crossref","is-referenced-by-count":45,"title":["Pure type systems formalized"],"prefix":"10.1007","author":[{"given":"James","family":"McKinna","sequence":"first","affiliation":[]},{"given":"Robert","family":"Pollack","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"20_CR1","doi-asserted-by":"crossref","unstructured":"Thorsten Altenkirch. A formalization of the strong normalization proof for System F in LEGO. In Proceedings of the International Conference on Typed Lambda Calculi and Applications, TLCA'93, March 1993.","DOI":"10.1007\/BFb0037095"},{"issue":"2","key":"20_CR2","doi-asserted-by":"crossref","first-page":"124","DOI":"10.1017\/S0956796800020025","volume":"1","author":"H. Barendregt","year":"1991","unstructured":"Henk Barendregt. Introduction to generalised type systems. J. Functional Programming, 1(2):124\u2013154, April 1991.","journal-title":"J. Functional Programming"},{"key":"20_CR3","doi-asserted-by":"crossref","unstructured":"Henk Barendregt. Lambda calculi with types. In Gabbai Abramsky and Maibaum, editors, Handbook of Logic in Computer Science, volume II. Oxford University Press, 1992.","DOI":"10.1093\/oso\/9780198537618.003.0002"},{"key":"20_CR4","volume-title":"PhD thesis","author":"S. Berardi","year":"1990","unstructured":"Stefano Berardi. Type Dependence and Constructive Mathematics. PhD thesis, Dipartimento di Informatica, Torino, Italy, 1990."},{"key":"20_CR5","doi-asserted-by":"crossref","unstructured":"Thierry Coquand. An algorithm for testing conversion in type theory. In G. Huet and G. D. Plotkin, editors, Logical Frameworks. Cambridge University Press, 1991.","DOI":"10.1017\/CBO9780511569807.011"},{"issue":"2","key":"20_CR6","doi-asserted-by":"crossref","first-page":"155","DOI":"10.1017\/S0956796800020037","volume":"1","author":"H. Geuvers","year":"1991","unstructured":"Herman Geuvers and Mark-Jan Nederhof. A modular proof of strong normalization for the calculus of constructions. Journal of Functional Programming, 1(2):155\u2013189, April 1991.","journal-title":"Journal of Functional Programming"},{"key":"20_CR7","doi-asserted-by":"crossref","unstructured":"G\u00e9rard Huet. The constructive engine. In The Calculus of Constructions; Documentation and users' guide. INRIA-Rocquencourt, Aug 1989. Technical Report 110.","DOI":"10.1142\/9789814368452_0004"},{"key":"20_CR8","unstructured":"Claire Jones. Completing the rationals and metric spaces in LEGO. In 2nd Workshop of Logical Frameworks, Edinburgh, pages 209\u2013222, May 1991. available by ftp."},{"key":"20_CR9","volume-title":"Technical Report ECS-LFCS-92-211, LFCS","author":"Z. Luo","year":"1992","unstructured":"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 EII9 3JZ, May 1992. Updated version."},{"key":"20_CR10","doi-asserted-by":"crossref","unstructured":"Zhaohui Luo. Program specification and data refinement in type theory. In TAPSOFT '91 (Volume 1), number 493 in Lecture Notes in Computer Science, pages 143\u2013168. Springer-Verlag, 1991.","DOI":"10.1007\/3-540-53982-4_9"},{"key":"20_CR11","doi-asserted-by":"crossref","unstructured":"James McKinna. Deliverables: a Categorical Approach to Program Development in Type Theory. PhD thesis, University of Edinburgh, 1992.","DOI":"10.1007\/3-540-57182-5_3"},{"key":"20_CR12","unstructured":"R. Pollack. Typechecking in pure type systems. In 1992 Workshop on Types for Proofs and Programs, B\u00e5stad, Sweden, pages 271\u2013288, June 1992. available by ftp."},{"key":"20_CR13","unstructured":"N. Shankar. A mechanical proof of the church-rosser theorem. Technical Report 45, Institute for Computing Science, University of Texas at Austin, March 1985."},{"key":"20_CR14","unstructured":"Jan Smith, Bengt Nordstr\u00f6m, and Kent Petersson. Programming in Martin-L\u00f6f's Type Theory. An Introduction. Oxford University Press, 1990."},{"key":"20_CR15","unstructured":"L.S. van Benthem Jutting. Typing in pure type systems. Information and Computation, 1992. To appear."},{"key":"20_CR16","unstructured":"L. van Benthem Jutting, James McKinna, and Robert Pollack. Typechecking in pure type systems. in preparation, 1992."}],"container-title":["Lecture Notes in Computer Science","Typed Lambda Calculi and Applications"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0037113.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,2,2]],"date-time":"2024-02-02T14:06:17Z","timestamp":1706882777000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0037113"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["3540565175"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/bfb0037113","relation":{},"subject":[]}}