{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,9]],"date-time":"2026-03-09T22:58:35Z","timestamp":1773097115311,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":17,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540617808","type":"print"},{"value":"9783540707226","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1996]]},"DOI":"10.1007\/3-540-61780-9_74","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T22:25:36Z","timestamp":1330295136000},"page":"249-264","source":"Crossref","is-referenced-by-count":8,"title":["A simple model construction for the Calculus of Constructions"],"prefix":"10.1007","author":[{"given":"M.","family":"Stefanova","sequence":"first","affiliation":[]},{"given":"H.","family":"Geuvers","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,6,7]]},"reference":[{"key":"17_CR1","unstructured":"T. Altenkirch. Constructions, Inductive Types and Strong Normalization. PhD thesis, Laboratory for the Foundations of Computer Science, University of Edinburgh, 1993."},{"key":"17_CR2","volume-title":"The Lambda Calculus: Its Syntax and Semantics","author":"H. P. Barendregt","year":"1984","unstructured":"H. P. Barendregt. The Lambda Calculus: Its Syntax and Semantics. North-Holland, Amsterdam, second, revised edition, 1984.","edition":"second, revised"},{"key":"17_CR3","doi-asserted-by":"crossref","unstructured":"H. P. Barendregt. Typed lambda calculi. In Abramski, editor, Handbook of Logic in Computer Science. Oxford University Press, 1992.","DOI":"10.1093\/oso\/9780198537618.003.0002"},{"key":"17_CR4","unstructured":"S. Berardi. Encoding of data types in pure construction calculus: a semantic justification. In G. Plotkin and G. Huet, editors, Logical Enviroments, pages 30\u201360, Edinburgh, 1992."},{"key":"17_CR5","doi-asserted-by":"crossref","first-page":"309","DOI":"10.1017\/S0960129500000244","volume":"3","author":"S. Berardi","year":"1993","unstructured":"S. Berardi. An application of per models to program extraction. Mathematical Structures in Computer Science, 3:309\u2013331, 1993.","journal-title":"Mathematical Structures in Computer Science"},{"key":"17_CR6","volume-title":"Technical report","author":"I. Bethke","year":"1995","unstructured":"I. Bethke and J. W. Klop. Collapsing partial combinatory algebras. Technical report, CWI, The Netherlands, 1995."},{"key":"17_CR7","unstructured":"J. H. Geuvers. Semantics for dependent types (the calculus of constructions) by a \u2018double\u2019 model construction. Technical report, Department of Computer Science, University of Eindhoven, 1995."},{"key":"17_CR8","doi-asserted-by":"crossref","unstructured":"J. H. Geuvers. A short and flexible proof of strong normalization for the calculus of constructions. In P. Dybjer, B. Nordstr\u00f6m, and J. Smith, editors, Types for Proofs and Programs, Int. Workshop TYPES '94, B\u00e1stad, Sweden, LNCS 996, pages 14\u201338, Edinburgh, 1995.","DOI":"10.1007\/3-540-60579-7_2"},{"issue":"2","key":"17_CR9","doi-asserted-by":"crossref","first-page":"155","DOI":"10.1017\/S0956796800020037","volume":"1","author":"J.H. Geuvers","year":"1991","unstructured":"J.H. Geuvers and M.J. Nederhof. A modular proof of strong normalization for the calculus of constructions. Journal of Functional Programming, 1(2):155\u2013189, 1991.","journal-title":"Journal of Functional Programming"},{"key":"17_CR10","doi-asserted-by":"crossref","unstructured":"J.M. E. Hyland and C.-H. L. Ong. Modified realizability and strong normalization proofs. In M. Bezem and J. F. Groote, editors, Typed Lambda Calculi and Applications, 1993.","DOI":"10.1007\/BFb0037106"},{"key":"17_CR11","unstructured":"J. M. E. Hyland and M. Pitts. The theory of constructions: Categorical semantics and topos-theoretic models. In Boulder, editor, AMS notes, 1987."},{"key":"17_CR12","doi-asserted-by":"crossref","first-page":"215","DOI":"10.1017\/S0960129500001298","volume":"1","author":"G. Longo","year":"1991","unstructured":"G. Longo and E. Moggi. Constructive natural deduction and its\u2019 \u03c9-set \u2018interpretation. Mathematical Structures in Computer Science, 1:215\u2013254, 1991.","journal-title":"Mathematical Structures in Computer Science"},{"key":"17_CR13","first-page":"107","volume":"90","author":"Z. Luo","year":"1991","unstructured":"Z. Luo. A higher-order calculus and theory abstraction. IC, 90:107\u2013137, 1991.","journal-title":"IC"},{"key":"17_CR14","doi-asserted-by":"crossref","unstructured":"J. C. Reynolds. Polymorphism is not set-theoretic. In G. Kahn, D. B. McQueen, and G. Plotkin, editors, Lecture Notes in Computer Science 173, 1984.","DOI":"10.1007\/3-540-13346-1_7"},{"key":"17_CR15","unstructured":"M.T. Stefanova. Schematic proof of strong normalization for barendregt's-cube, 1995. Submitted, also available at http:\/\/www.cs.kun.nl\/\u223cmilena."},{"key":"17_CR16","volume-title":"Progress in Theoretical Computer Science","author":"T. Streicher","year":"1991","unstructured":"T. Streicher. Semantics of Type Theory. Correctness, Completeness and Independence Results. Progress in Theoretical Computer Science. Birkh\u00e4user, Boston, 1991."},{"issue":"2","key":"17_CR17","doi-asserted-by":"crossref","first-page":"395","DOI":"10.1016\/0304-3975(92)90021-7","volume":"103","author":"T. Streicher","year":"1992","unstructured":"T. Streicher. Independence of the induction principle and the axiom of choice in the pure calculus of constructions. TCS, 103(2):395\u2013409, 1992.","journal-title":"TCS"}],"container-title":["Lecture Notes in Computer Science","Types for Proofs and Programs"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-61780-9_74.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,4,20]],"date-time":"2024-04-20T17:47:18Z","timestamp":1713635238000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-61780-9_74"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1996]]},"ISBN":["9783540617808","9783540707226"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/3-540-61780-9_74","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[1996]]}}}