{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T15:58:59Z","timestamp":1725551939841},"publisher-location":"Berlin, Heidelberg","reference-count":29,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642122507"},{"type":"electronic","value":"9783642122514"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2010]]},"DOI":"10.1007\/978-3-642-12251-4_17","type":"book-chapter","created":{"date-parts":[[2010,4,9]],"date-time":"2010-04-09T19:32:42Z","timestamp":1270841562000},"page":"224-239","source":"Crossref","is-referenced-by-count":4,"title":["Towards Normalization by Evaluation for the \u03b2\u03b7-Calculus of Constructions"],"prefix":"10.1007","author":[{"given":"Andreas","family":"Abel","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"17_CR1","doi-asserted-by":"crossref","unstructured":"Abel, A.: Towards Normalization by Evaluation for the Calculus of Constructions (Extended Version). Available on the author\u2019s homepage (2010)","DOI":"10.1007\/978-3-642-12251-4_17"},{"issue":"4","key":"17_CR2","doi-asserted-by":"publisher","first-page":"375","DOI":"10.1017\/S0956796800000186","volume":"1","author":"M. Abadi","year":"1991","unstructured":"Abadi, M., Cardelli, L., Curien, P.-L., L\u00e9vy, J.-J.: Explicit substitutions. JFP\u00a01(4), 375\u2013416 (1991)","journal-title":"JFP"},{"key":"17_CR3","first-page":"3","volume-title":"LICS 2007","author":"A. Abel","year":"2007","unstructured":"Abel, A., Coquand, T., Dybjer, P.: Normalization by evaluation for Martin-L\u00f6f Type Theory with typed equality judgements. In: LICS 2007, pp. 3\u201312. IEEE CS Press, Los Alamitos (2007)"},{"key":"17_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"29","DOI":"10.1007\/978-3-540-70594-9_4","volume-title":"Mathematics of Program Construction","author":"A. Abel","year":"2008","unstructured":"Abel, A., Coquand, T., Dybjer, P.: Verifying a semantic \u03b2\u03b7-conversion test for Martin-L\u00f6f type theory. In: Audebaud, P., Paulin-Mohring, C. (eds.) MPC 2008. LNCS, vol.\u00a05133, pp. 29\u201356. Springer, Heidelberg (2008)"},{"key":"17_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1007\/978-3-642-02273-9_3","volume-title":"Typed Lambda Calculi and Applications","author":"A. Abel","year":"2009","unstructured":"Abel, A., Coquand, T., Pagano, M.: A modular type-checking algorithm for type theory with singleton types and proof irrelevance. In: Curien, P.-L. (ed.) TLCA 2009. LNCS, vol.\u00a05608, pp. 5\u201319. Springer, Heidelberg (2009)"},{"issue":"2","key":"17_CR6","doi-asserted-by":"publisher","first-page":"219","DOI":"10.1017\/S0956796805005770","volume":"16","author":"R. Adams","year":"2006","unstructured":"Adams, R.: Pure type systems with judgemental equality. JFP\u00a016(2), 219\u2013246 (2006)","journal-title":"JFP"},{"key":"17_CR7","unstructured":"Barras, B.: Sets in Coq, Coq in sets. In: The 1st Coq Workshop, Proceedings, Technische Universit\u00e4t M\u00fcnchen (2009)"},{"key":"17_CR8","unstructured":"Barras, B., Werner, B.: Coq in Coq. Available on the WWW (1997)"},{"key":"17_CR9","doi-asserted-by":"crossref","unstructured":"Cartmell, J.: Generalised algebraic theories and contextual categories. In: APAL, pp. 32\u2013209 (1986)","DOI":"10.1016\/0168-0072(86)90053-9"},{"key":"17_CR10","unstructured":"Coquand, T., Gallier, J.: A proof of strong normalization for the theory of constructions using a kripke-like interpretation. In: Proceedings of the First Workshop on Logical Frameworks (1990)"},{"key":"17_CR11","unstructured":"Chapman, J.: Type Checking and Normalization. PhD thesis, School of Computer Science, University of Nottingham (2009)"},{"key":"17_CR12","series-title":"Lecture Notes in Computer Science","first-page":"167","volume-title":"Mathematics of Program Construction","author":"T. Coquand","year":"1995","unstructured":"Coquand, T.: An algorithm for type-checking dependent types. In: M\u00f6ller, B. (ed.) MPC 1995. LNCS, vol.\u00a0947, pp. 167\u2013177. Springer, Heidelberg (1995)"},{"key":"17_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1007\/978-3-540-74464-1_7","volume-title":"Types for Proofs and Programs","author":"N.A. Danielsson","year":"2007","unstructured":"Danielsson, N.A.: A formalisation of a dependently typed language as an inductive-recursive family. In: Altenkirch, T., McBride, C. (eds.) TYPES 2006. LNCS, vol.\u00a04502, pp. 93\u2013109. Springer, Heidelberg (2007)"},{"key":"17_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"14","DOI":"10.1007\/3-540-60579-7_2","volume-title":"Types for Proofs and Programs","author":"H. Geuvers","year":"1995","unstructured":"Geuvers, H.: A short and flexible proof of strong normalization for the Calculus of Constructions. In: Smith, J., Dybjer, P., Nordstr\u00f6m, B. (eds.) TYPES 1994. LNCS, vol.\u00a0996, pp. 14\u201338. Springer, Heidelberg (1995)"},{"key":"17_CR15","series-title":"SIGPLAN Notices","doi-asserted-by":"publisher","first-page":"235","DOI":"10.1145\/581478.581501","volume-title":"ICFP 2002","author":"B. Gr\u00e9goire","year":"2002","unstructured":"Gr\u00e9goire, B., Leroy, X.: A compiled implementation of strong reduction. In: ICFP 2002. SIGPLAN Notices, vol.\u00a037, pp. 235\u2013246. ACM, New York (2002)"},{"issue":"2","key":"17_CR16","first-page":"155","volume":"1","author":"H. Geuvers","year":"1991","unstructured":"Geuvers, H., Nederhof, M.-J.: Modular proof of strong normalization for the calculus of constructions. JFP\u00a01(2), 155\u2013189 (1991)","journal-title":"JFP"},{"key":"17_CR17","unstructured":"Goguen, H.: A Typed Operational Semantics for Type Theory. PhD thesis, University of Edinburgh. Available as LFCS Report ECS-LFCS-94-304 (1994)"},{"key":"17_CR18","unstructured":"Gonthier, G.: A computer-checked proof of the four colour theorem. Technical report, Microsoft Research (2004), http:\/\/research.microsoft.com\/~gonthier\/"},{"key":"17_CR19","unstructured":"Granstr\u00f6m, J.: Reference and Computation in Intuitionistic Type Theory. PhD thesis, Mathematical Logic, Uppsala University (2009)"},{"key":"17_CR20","series-title":"Final version in anniversary volume Theoretical Computer Science in memory of Gift Siromoney","volume-title":"2nd European Symposium on Programming","author":"G. Huet","year":"1989","unstructured":"Huet, G.: The constructive engine. In: Narasimhan, R. (ed.) 2nd European Symposium on Programming, Nancy, March 1988. Final version in anniversary volume Theoretical Computer Science in memory of Gift Siromoney. World Scientific Publishing, Singapore (1989)"},{"key":"17_CR21","unstructured":"INRIA. The Coq Proof Assistant Reference Manual. INRIA, version 8.2 edition (2008), http:\/\/coq.inria.fr\/"},{"key":"17_CR22","doi-asserted-by":"publisher","first-page":"42","DOI":"10.1145\/1111037.1111042","volume-title":"POPL 2006","author":"X. Leroy","year":"2006","unstructured":"Leroy, X.: Formal certification of a compiler back-end or: programming a compiler with a proof assistant. In: POPL 2006, pp. 42\u201354. ACM, New York (2006)"},{"key":"17_CR23","first-page":"386","volume-title":"LICS 1989","author":"Z. Luo","year":"1989","unstructured":"Luo, Z.: ECC, an Extended Calculus of Constructions. In: LICS 1989, pp. 386\u2013395. IEEE CS Press, Los Alamitos (1989)"},{"key":"17_CR24","doi-asserted-by":"crossref","unstructured":"Miquel, A.: A model for impredicative type systems, universes, intersection types and subtyping. In: LICS, pp. 18\u201329 (2000)","DOI":"10.1109\/LICS.2000.855752"},{"key":"17_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"240","DOI":"10.1007\/3-540-39185-1_14","volume-title":"Types for Proofs and Programs","author":"A. Miquel","year":"2003","unstructured":"Miquel, A., Werner, B.: The not so simple proof-irrelevant model of CC. In: Geuvers, H., Wiedijk, F. (eds.) TYPES 2002. LNCS, vol.\u00a02646, pp. 240\u2013258. Springer, Heidelberg (2003)"},{"key":"17_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"313","DOI":"10.1007\/3-540-58085-9_82","volume-title":"Types for Proofs and Programs","author":"R. Pollack","year":"1994","unstructured":"Pollack, R.: Closure under alpha-conversion. In: Barendregt, H., Nipkow, T. (eds.) TYPES 1993. LNCS, vol.\u00a0806, pp. 313\u2013332. Springer, Heidelberg (1994)"},{"key":"17_CR27","unstructured":"Pollack, R.: The constructive engine. Talk presented at the TYPES Workshop Curry-Howard Implementation Techniques - Connecting Humans And Theorem provers, CHIT-CHAT 2006, Radboud University, Nijmegen, The Netherlands (2006)"},{"key":"17_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"249","DOI":"10.1007\/3-540-61780-9_74","volume-title":"Types for Proofs and Programs","author":"M. Stefanova","year":"1996","unstructured":"Stefanova, M., Geuvers, H.: A simple model construction for the calculus of constructions. In: Berardi, S., Coppo, M. (eds.) TYPES 1995. LNCS, vol.\u00a01158, pp. 249\u2013264. Springer, Heidelberg (1996)"},{"key":"17_CR29","unstructured":"Werner, B.: A normalization proof for an impredicative type system with large eliminations over integers. In: TYPES 1992, pp. 341\u2013357 (1992)"}],"container-title":["Lecture Notes in Computer Science","Functional and Logic Programming"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-12251-4_17.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,23]],"date-time":"2020-11-23T21:51:59Z","timestamp":1606168319000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-12251-4_17"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642122507","9783642122514"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-12251-4_17","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2010]]}}}