{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T22:48:23Z","timestamp":1725490103558},"publisher-location":"Berlin, Heidelberg","reference-count":17,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540745907"},{"type":"electronic","value":"9783540745914"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-74591-4_27","type":"book-chapter","created":{"date-parts":[[2007,8,22]],"date-time":"2007-08-22T14:49:52Z","timestamp":1187794192000},"page":"368-382","source":"Crossref","is-referenced-by-count":7,"title":["Simple Types in Type Theory: Deep and Shallow Encodings"],"prefix":"10.1007","author":[{"given":"Fran\u00e7ois","family":"Garillot","sequence":"first","affiliation":[]},{"given":"Benjamin","family":"Werner","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"27_CR1","doi-asserted-by":"crossref","unstructured":"Altenkirch, T., Dybjer, P., Hofmann, M., Scott, P.J.: Normalization by evaluation for typed lambda calculus with coproducts. In: LICS, pp. 303\u2013310 (2001)","DOI":"10.1109\/LICS.2001.932506"},{"key":"27_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"91","DOI":"10.1007\/BFb0037100","volume-title":"Typed Lambda Calculi and Applications","author":"U. Berger","year":"1993","unstructured":"Berger, U.: Program extraction from normalization proofs. In: Bezem, M., Groote, J.F. (eds.) TLCA 1993. LNCS, vol.\u00a0664, pp. 91\u2013106. Springer, Heidelberg (1993)"},{"issue":"1","key":"27_CR3","doi-asserted-by":"publisher","first-page":"25","DOI":"10.1007\/s11225-006-6604-5","volume":"82","author":"U. Berger","year":"2006","unstructured":"Berger, U., Berghofer, S., Letouzey, P., Schwichtenberg, H.: Program extraction from normalization proofs. Studia Logica\u00a082(1), 25\u201349 (2006)","journal-title":"Studia Logica"},{"key":"27_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"117","DOI":"10.1007\/3-540-49254-2_4","volume-title":"Prospects for Hardware Foundations","author":"U. Berger","year":"1998","unstructured":"Berger, U., Eberl, M., Schwichtenberg, H.: Normalisation by evaluation. In: M\u00f6ller, B., Tucker, J.V. (eds.) Prospects for Hardware Foundations. LNCS, vol.\u00a01546, pp. 117\u2013137. Springer, Heidelberg (1998)"},{"issue":"1","key":"27_CR5","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1016\/S0890-5401(03)00014-2","volume":"183","author":"U. Berger","year":"2003","unstructured":"Berger, U., Eberl, M., Schwichtenberg, H.: Term rewriting for normalization by evaluation. Inf. Comput.\u00a0183(1), 19\u201342 (2003)","journal-title":"Inf. Comput."},{"key":"27_CR6","first-page":"203","volume-title":"LICS","author":"U. Berger","year":"1991","unstructured":"Berger, U., Schwichtenberg, H.: An inverse of the evaluation functional for typed lambda-calculus. In: LICS, pp. 203\u2013211. IEEE Computer Society Press, Los Alamitos (1991)"},{"key":"27_CR7","series-title":"Lecture Notes in Computer Science","volume-title":"Proceedings of TYPES 2006","author":"V. Capretta","year":"2007","unstructured":"Capretta, V., Felty, A.: Combining de bruijn indices and higher-order abstract syntax in coq. In: Altenkirch, T., McBride, C. (eds.) Proceedings of TYPES 2006. LNCS, Springer, Heidelberg (2007)"},{"key":"27_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"91","DOI":"10.1007\/BFb0049326","volume-title":"Computer Science Logic","author":"C. Coquand","year":"1994","unstructured":"Coquand, C.: From semantics to rules: A machine assisted analysis. In: Meinke, K., B\u00f6rger, E., Gurevich, Y. (eds.) CSL 1993. LNCS, vol.\u00a0832, pp. 91\u2013105. Springer, Heidelberg (1994)"},{"issue":"1","key":"27_CR9","doi-asserted-by":"publisher","first-page":"57","DOI":"10.1023\/A:1019964114625","volume":"15","author":"C. Coquand","year":"2002","unstructured":"Coquand, C.: A formalised proof of the soundness and completeness of a simply typed lambda-calculus with explicit substitutions. Higher-Order and Symbolic Computation\u00a015(1), 57\u201390 (2002)","journal-title":"Higher-Order and Symbolic Computation"},{"issue":"6","key":"27_CR10","doi-asserted-by":"publisher","first-page":"673","DOI":"10.1017\/S0956796801004166","volume":"11","author":"O. Danvy","year":"2001","unstructured":"Danvy, O., Rhiger, M., Rose, K.H.: Normalization by evaluation with typed abstract syntax. J. Funct. Program.\u00a011(6), 673\u2013680 (2001)","journal-title":"J. Funct. Program."},{"key":"27_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"147","DOI":"10.1007\/3-540-62688-3_34","volume-title":"Typed Lambda Calculi and Applications","author":"J. Despeyroux","year":"1997","unstructured":"Despeyroux, J., Pfenning, F., Sch\u00fcrmann, C.: Primitive recursion for higher-order abstract syntax. In: de Groote, P., Hindley, J.R. (eds.) TLCA 1997. LNCS, vol.\u00a01210, pp. 147\u2013163. Springer, Heidelberg (1997)"},{"key":"27_CR12","unstructured":"Gonthier, G.: A computer-checked proof of the four colour theorem (2005), available on \n                  \n                    http:\/\/research.microsoft.com\/~gonthier\/"},{"key":"27_CR13","unstructured":"Gonthier, G.: Notations of the four colour theorem proof (2005), available on \n                  \n                    http:\/\/research.microsoft.com\/~gonthier\/"},{"issue":"4","key":"27_CR14","doi-asserted-by":"publisher","first-page":"405","DOI":"10.2307\/421172","volume":"2","author":"J.-L. Krivine","year":"1996","unstructured":"Krivine, J.-L.: Une preuve formelle et intuitionniste du th\u00e9or\u00e8me de compl\u00e9tude de la logique classique. Bulletin of Symbolic Logic\u00a02(4), 405\u2013421 (1996)","journal-title":"Bulletin of Symbolic Logic"},{"key":"27_CR15","doi-asserted-by":"crossref","unstructured":"Pfenning, F., Elliott, C.: Higher-order abstract syntax. In: PLDI, pp. 199\u2013208 (1988)","DOI":"10.1145\/53990.54010"},{"issue":"1-2","key":"27_CR16","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/S0304-3975(00)00418-7","volume":"266","author":"C. Sch\u00fcrmann","year":"2001","unstructured":"Sch\u00fcrmann, C., Despeyroux, J., Pfenning, F.: Primitive recursion for higher-order abstract syntax. Theor. Comput. Sci.\u00a0266(1-2), 1\u201357 (2001)","journal-title":"Theor. Comput. Sci."},{"key":"27_CR17","doi-asserted-by":"publisher","first-page":"317","DOI":"10.1016\/0304-3975(88)90149-1","volume":"59","author":"A. Stoughton","year":"1988","unstructured":"Stoughton, A.: Substitution revisited. Theor. Comput. Sci.\u00a059, 317\u2013325 (1988)","journal-title":"Theor. Comput. Sci."}],"container-title":["Lecture Notes in Computer Science","Theorem Proving in Higher Order Logics"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-74591-4_27.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T10:28:11Z","timestamp":1619519291000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-74591-4_27"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540745907","9783540745914"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-74591-4_27","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[]}}