{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T15:58:57Z","timestamp":1725551937596},"publisher-location":"Berlin, Heidelberg","reference-count":14,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642122507"},{"type":"electronic","value":"9783642122514"}],"license":[{"start":{"date-parts":[[2010,1,1]],"date-time":"2010-01-01T00:00:00Z","timestamp":1262304000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2010]]},"DOI":"10.1007\/978-3-642-12251-4_16","type":"book-chapter","created":{"date-parts":[[2010,4,9]],"date-time":"2010-04-09T23:32:42Z","timestamp":1270855962000},"page":"207-223","source":"Crossref","is-referenced-by-count":0,"title":["Internal Normalization, Compilation and Decompilation for System ${\\mathcal F}_{\\beta\\eta}$"],"prefix":"10.1007","author":[{"given":"Stefano","family":"Berardi","sequence":"first","affiliation":[]},{"given":"Makoto","family":"Tatsuta","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"16_CR1","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"497","DOI":"10.1007\/978-3-540-89439-1_35","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"A. Abel","year":"2008","unstructured":"Abel, A.: Weak beta-Normalization and Normalization by Evaluation for System F. In: Cervesato, I., Veith, H., Voronkov, A. (eds.) LPAR 2008. LNCS (LNAI), vol.\u00a05330, pp. 497\u2013511. Springer, Heidelberg (2008)"},{"key":"16_CR2","unstructured":"Berardi, S., Tatsuta, M.: Internal Normalization, Compilation and Decompilation for System \n                      \n                        \n                      \n                      ${\\mathcal F}_{\\beta\\eta}$\n                     (full paper). Draft, \n                      \n                        http:\/\/www.di.unito.it\/~stefano\/CompletenessF.pdf"},{"key":"16_CR3","doi-asserted-by":"crossref","unstructured":"Berger, U., Eberl, M., Schwichtenberg, H.: Normalisation by Evaluation. In: Prospects for Hardware Foundations, pp. 117\u2013137 (1998)","DOI":"10.1007\/3-540-49254-2_4"},{"issue":"1","key":"16_CR4","doi-asserted-by":"publisher","first-page":"407","DOI":"10.1016\/S0304-3975(01)00379-6","volume":"290","author":"F. Barbanera","year":"2003","unstructured":"Barbanera, F., Berardi, S.: A full continuous model of polymorphism. Theor. Comput. Sci.\u00a0290(1), 407\u2013428 (2003)","journal-title":"Theor. Comput. Sci."},{"issue":"6","key":"16_CR5","doi-asserted-by":"publisher","first-page":"823","DOI":"10.1017\/S0960129502003778","volume":"12","author":"S. Berardi","year":"2002","unstructured":"Berardi, S., Berline, C.: \u03b2\u03b7-Complete Models for System F. Mathematical Structures in Computer Science\u00a012(6), 823\u2013874 (2002)","journal-title":"Mathematical Structures in Computer Science"},{"issue":"1","key":"16_CR6","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/j.tcs.2003.11.011","volume":"315","author":"S. Berardi","year":"2004","unstructured":"Berardi, S., Berline, C.: Building continuous webbed models for system F. Theor. Comput. Sci.\u00a0315(1), 3\u201334 (2004)","journal-title":"Theor. Comput. Sci."},{"key":"16_CR7","series-title":"LNM","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1007\/BFb0103100","volume-title":"Higher Set Theory","author":"H. Friedman","year":"1978","unstructured":"Friedman, H.: Classically and Intuitionistically Provably Recursive Functions. In: Scott, D.S., Muller, G.H. (eds.) Higher Set Theory. LNM, vol.\u00a0699, pp. 21\u201328. Springer, Heidelberg (1978)"},{"key":"16_CR8","unstructured":"Joly, T.: Codage, Separabilite et Representation, These de doctorat, Universite de Paris VII (2000), \n                      \n                        http:\/\/www.cs.ru.nl\/~joly\/these.ps.gz"},{"key":"16_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"368","DOI":"10.1007\/978-3-540-74591-4_27","volume-title":"Theorem Proving in Higher Order Logics","author":"F. Garillot","year":"2007","unstructured":"Garillot, F., Werner, B.: Simple Types in Type Theory: Deep and Shallow Encodings. In: Schneider, K., Brandt, J. (eds.) TPHOLs 2007. LNCS, vol.\u00a04732, pp. 368\u2013382. Springer, Heidelberg (2007)"},{"issue":"2","key":"16_CR10","first-page":"215","volume":"1","author":"G. Longo","year":"1991","unstructured":"Longo, G., Moggi, E.: Constructive Natural Deduction and its \u2018Omega-Set\u2019 Interpretation. MSCS\u00a01(2), 215\u2013254 (1991)","journal-title":"MSCS"},{"key":"16_CR11","doi-asserted-by":"crossref","unstructured":"Mitchell, J.C.: Semantic Models For Second-Order Lambda Calculus. In: 25th Annual Symposium on Foundations of Computer Science, pp. 289\u2013299 (1984)","DOI":"10.1109\/SFCS.1984.715927"},{"key":"16_CR12","unstructured":"Moggi, E., Statman, R.: The Maximum Consistent Theory of Second Order Lambda Calculus. e-mail message to the \u201cTypes\u201d net (July 24, 1986), \n                      \n                        http:\/\/www.di.unito.it\/~stefano\/MoggiStatman1986.zip"},{"key":"16_CR13","series-title":"SIGPLAN Notices","first-page":"199","volume-title":"Proceedings of the ACM SIGPLAN 1988 PLDI","author":"F. Pfenning","year":"1988","unstructured":"Pfenning, F., Elliott, C.: Higher-order abstract syntax. In: Wexelblat, R.L. (ed.) Proceedings of the ACM SIGPLAN 1988 PLDI. SIGPLAN Notices, vol.\u00a023(7), pp. 199\u2013208. ACM Press, New York (1988)"},{"key":"16_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"345","DOI":"10.1007\/3-540-50940-2_46","volume-title":"TAPSOFT \u201989. Proceedings of the International Joint Conference on Theory and Practice of Software Development Barcelona, Spain, March 13-17, 1989","author":"F. Pfenning","year":"1989","unstructured":"Pfenning, F., Lee, P.: LEAP: A language with eval and polymorphism. In: D\u00edaz, J., Orejas, F. (eds.) TAPSOFT 1989 and CCIPL 1989. LNCS, vol.\u00a0352, pp. 345\u2013359. Springer, Heidelberg (1989)"}],"container-title":["Lecture Notes in Computer Science","Functional and Logic Programming"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-12251-4_16","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,19]],"date-time":"2019-05-19T18:09:55Z","timestamp":1558289395000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-12251-4_16"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642122507","9783642122514"],"references-count":14,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-12251-4_16","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2010]]}}}