{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,9]],"date-time":"2026-05-09T02:42:03Z","timestamp":1778294523815,"version":"3.51.4"},"publisher-location":"Berlin\/Heidelberg","reference-count":20,"publisher":"Springer-Verlag","isbn-type":[{"value":"3540565175","type":"print"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/bfb0037095","type":"book-chapter","created":{"date-parts":[[2006,1,25]],"date-time":"2006-01-25T15:21:36Z","timestamp":1138202496000},"page":"13-28","source":"Crossref","is-referenced-by-count":27,"title":["A formalization of the strong normalization proof for System F in LEGO"],"prefix":"10.1007","author":[{"given":"Thorsten","family":"Altenkirch","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"2_CR1","unstructured":"Thorsten Altenkirch. Impredicative representations of categorical datatypes, thesis proposal, October 1990."},{"key":"2_CR2","unstructured":"Henk Barendregt et al. Summer school on \u03bb calculus, 1991."},{"key":"2_CR3","unstructured":"Stefano Berardi. Girard's normalisation proof in LEGO. unpublished draft, 1991."},{"key":"2_CR4","unstructured":"Catarina Coquand. A proof of normalization for simply typed lambda calculus written in ALF. In Workshop on Logical Frameworks, 1992. Preliminary Proceedings."},{"key":"2_CR5","unstructured":"Thierry Coquand. Pattern matching with dependent types. In Workshop on Logical Frameworks, 1992. Preliminary Proceedings."},{"key":"2_CR6","doi-asserted-by":"crossref","unstructured":"Thierry Coquand and Christine Paulin. Inductively defined types. In Peter Dybjer et al., editors, Proceedings of the Workshop on Programming Logic, 1989.","DOI":"10.1007\/3-540-52335-9_47"},{"key":"2_CR7","unstructured":"Gilles Dowek et al. The Coq Proof Assistant User's Guide. INRIA-Rocquencourt \u2014 CNRS-ENS Lyon, 1991. Version 5.6."},{"key":"2_CR8","doi-asserted-by":"crossref","unstructured":"N.G. de Bruijn. Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the church-rosser theorem. Indag. Math., 34, 1972.","DOI":"10.1016\/1385-7258(72)90034-0"},{"key":"2_CR9","unstructured":"J.H. Gallier. On Girard's \u201cCandidats de Reducibilit\u00e9\u201d. In Piergiogio Oddifreddi, editor, Logic and Computer Science. Academic Press, 1990."},{"key":"2_CR10","unstructured":"J.-Y. Girard, Y. Lafont, and P. Taylor. Proofs and Types. Cambridge University Press, 1989."},{"key":"2_CR11","unstructured":"Martin Hofmann. Formal development of functional programs in type theory \u2014 a case study. LFCS Report ECS-LFCS-92-228, University of Edinburgh, 1992."},{"issue":"4","key":"2_CR12","doi-asserted-by":"crossref","first-page":"797","DOI":"10.1145\/322217.322230","volume":"27","author":"G. Huet","year":"1980","unstructured":"G\u00e9rard Huet. Confluent reductions. JACM, 27(4):797\u2013821, 1980.","journal-title":"JACM"},{"key":"2_CR13","unstructured":"G\u00e9rard Huet. Initiation au lambda calcul. Lecture notes, 1992."},{"key":"2_CR14","unstructured":"Zhaohui Luo and Robert Pollack. The LEGO proof development system: A user's manual. LFCS report ECS-LFCS-92-211, University of Edinburgh, 1992."},{"key":"2_CR15","unstructured":"Zhaohui Luo. An Extended Calculus of Constructions. PhD thesis, University of Edinburgh, 1990."},{"key":"2_CR16","unstructured":"Lena Magnusson. The new implementation of ALF. In Workshop on Logical Frameworks, 1992. Preliminary Proceedings."},{"key":"2_CR17","unstructured":"N.P. Mendler. Inductive Definition in Type Theory. PhD thesis, Cornell University, 1988."},{"key":"2_CR18","unstructured":"Bengt Nordstr\u00f6m, Kent Petersson, and Jan Smith. Programming in Martin-L\u00f6f's Type Theory. Oxford University Press, 1990."},{"key":"2_CR19","unstructured":"Frank Pfenning. On the undecidability of partial polymorphic type reconstruction. Technical Report CMU-CS-92-105, Carnegie Mellon University, January 1992."},{"key":"2_CR20","unstructured":"Benjamin Werner. A normalization proof for an impredicative type system with large eliminations over integers. In Workshop on Logical Frameworks, 1992. Preliminary Proceedings."}],"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\/BFb0037095.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,7]],"date-time":"2025-01-07T11:51:12Z","timestamp":1736250672000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0037095"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["3540565175"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/bfb0037095","relation":{},"subject":[]}}