{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,28]],"date-time":"2025-03-28T04:50:13Z","timestamp":1743137413160,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":28,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783662468227"},{"type":"electronic","value":"9783662468234"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-662-46823-4_16","type":"book-chapter","created":{"date-parts":[[2015,4,18]],"date-time":"2015-04-18T01:40:54Z","timestamp":1429321254000},"page":"186-200","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Certifying Supercompilation for Martin-L\u00f6f\u2019s Type Theory"],"prefix":"10.1007","author":[{"given":"Ilya","family":"Klyuchnikov","sequence":"first","affiliation":[]},{"given":"Sergei","family":"Romanenko","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2015,4,19]]},"reference":[{"issue":"6","key":"16_CR1","doi-asserted-by":"publisher","first-page":"811","DOI":"10.1017\/S0956796800002008","volume":"6","author":"MH S\u00f8rensen","year":"1996","unstructured":"S\u00f8rensen, M.H., Gl\u00fcck, R., Jones, N.D.: A positive supercompiler. J. Funct. Program. 6(6), 811\u2013838 (1996)","journal-title":"J. Funct. Program."},{"key":"16_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"246","DOI":"10.1007\/3-540-47018-2_10","volume-title":"Partial Evaluation: Practice and Theory","author":"MH S\u00f8rensen","year":"1999","unstructured":"S\u00f8rensen, M.H., Gl\u00fcck, R.: Introduction to supercompilation. In: Hatcliff, J., Thiemann, P. (eds.) DIKU 1998. LNCS, vol. 1706, pp. 246\u2013270. Springer, Heidelberg (1999)"},{"issue":"3","key":"16_CR3","doi-asserted-by":"publisher","first-page":"292","DOI":"10.1145\/5956.5957","volume":"8","author":"VF Turchin","year":"1986","unstructured":"Turchin, V.F.: The concept of a supercompiler. ACM Trans. Program. Lang. Syst. (TOPLAS) 8(3), 292\u2013325 (1986)","journal-title":"ACM Trans. Program. Lang. Syst. (TOPLAS)"},{"key":"16_CR4","unstructured":"Turchin, V.F.: The language Refal: the theory of compilation and metasystem analysis. Technical report 20, Courant Institute of Mathematical Sciences (1980)"},{"issue":"1","key":"16_CR5","doi-asserted-by":"publisher","first-page":"14","DOI":"10.1134\/S0361768807010033","volume":"33","author":"A Lisitsa","year":"2007","unstructured":"Lisitsa, A., Nemytykh, A.: Verification as a parameterized testing. Program. Comput. Softw. 33(1), 14\u201323 (2007)","journal-title":"Program. Comput. Softw."},{"key":"16_CR6","unstructured":"Klimov, A., Klyuchnikov, I., Romanenko, S.: Automatic verification of counter systems via domain-specific multi-result supercompilation. In: [27]"},{"key":"16_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1007\/978-3-642-11486-1_17","volume-title":"Perspectives of Systems Informatics","author":"I Klyuchnikov","year":"2010","unstructured":"Klyuchnikov, I., Romanenko, S.: Proving the equivalence of higher-order terms by means of supercompilation. In: Pnueli, A., Virbitskaite, I., Voronkov, A. (eds.) PSI 2009. LNCS, vol. 5947, pp. 193\u2013205. Springer, Heidelberg (2010)"},{"key":"16_CR8","unstructured":"Klyuchnikov, I.: Inferring and proving properties of functional programs by means of supercompilation. Ph.D. thesis, Keldysh Institute of Applied Mathematics (2010)"},{"key":"16_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"227","DOI":"10.1007\/3-540-62064-8_20","volume-title":"Perspectives of System Informatics","author":"VF Turchin","year":"1996","unstructured":"Turchin, V.F.: Supercompilation: techniques and results. In: Bjorner, D., Broy, M., Pottosin, I.V. (eds.) PSI 1996. LNCS, vol. 1181, pp. 227\u2013248. Springer, Heidelberg (1996)"},{"key":"16_CR10","unstructured":"Klyuchnikov, I., Romanenko, S.: Towards higher-level supercompilation. In: [28]"},{"key":"16_CR11","unstructured":"Mendel-Gleason, G., Hamilton, G.: Development of the productive forces. In: [27]"},{"key":"16_CR12","unstructured":"Klyuchnikov, I.: Supercompiler HOSC: proof of correctness. Preprint 31, KIAM, Moscow (2010). http:\/\/library.keldysh.ru\/preprint.asp?id=2010-31"},{"key":"16_CR13","unstructured":"Krustev, D.: A simple supercompiler formally verified in Coq. In: [28], pp. 102\u2013127"},{"key":"16_CR14","volume-title":"Interactive Theorem Proving and Program Development: Coq\u2019Art The Calculus of Inductive Constructions","author":"Y Bertot","year":"2010","unstructured":"Bertot, Y., Castran, P.: Interactive Theorem Proving and Program Development: Coq\u2019Art The Calculus of Inductive Constructions. Springer, Heidelberg (2010)"},{"key":"16_CR15","unstructured":"The agda wiki (2013). http:\/\/wiki.portal.chalmers.se\/agda\/"},{"key":"16_CR16","unstructured":"Klyuchnikov, I., Romanenko, S.: TT Lite: A Supercompiler for Martin-L\u00f6f\u2019s Type Theory. Preprint, KIAM, Moscow (2013). http:\/\/library.keldysh.ru\/\/preprint.asp?lg=e&id=2013-73"},{"key":"16_CR17","volume-title":"Intuitionistic Type Theory","author":"P Martin-Lof","year":"1984","unstructured":"Martin-Lof, P.: Intuitionistic Type Theory. Bibliopolis, Naples (1984)"},{"key":"16_CR18","unstructured":"Pardo, A., da Rosa, S.: Program transformation in Martin-L\u00f6f\u2019s type theory. In: CADE-12, Workshop on Proof-Search in Type-Theoretic Languages (1994)"},{"key":"16_CR19","volume-title":"Programming in Martin-L\u00f6f\u2019s Type Theory","author":"B Nordstr\u00f6m","year":"1990","unstructured":"Nordstr\u00f6m, B., Petersson, K., Smith, J.M.: Programming in Martin-L\u00f6f\u2019s Type Theory. Oxford University Press, Oxford (1990)"},{"key":"16_CR20","volume-title":"Type Theory and Functional Programming","author":"S Thompson","year":"1991","unstructured":"Thompson, S.: Type Theory and Functional Programming. Addison Wesley Longman Publishing Co. Inc., Redwood City (1991)"},{"key":"16_CR21","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139342131","volume-title":"Practical Foundations for Programming Languages","author":"R Harper","year":"2012","unstructured":"Harper, R.: Practical Foundations for Programming Languages. Cambridge University Press, New York (2012)"},{"key":"16_CR22","first-page":"1001","volume":"21","author":"A L\u00f6h","year":"2010","unstructured":"L\u00f6h, A., McBride, C., Swierstra, W.: A tutorial implementation of a dependently typed lambda calculus. Fundamenta Informaticae 21, 1001\u20131032 (2010)","journal-title":"Fundamenta Informaticae"},{"key":"16_CR23","unstructured":"Klyuchnikov, I.G., Romanenko, S.A.: MRSC: A Toolkit for Building Multi-result Supercompilers. Preprint 77, KIAM (2011). http:\/\/library.keldysh.ru\/preprint.asp?lg=e&id=2011-77"},{"key":"16_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"62","DOI":"10.1007\/3-540-46562-6_6","volume-title":"Perspectives of System Informatics","author":"ND Jones","year":"2000","unstructured":"Jones, N.D.: The essence of program transformation by partial evaluation and driving. In: Bjorner, D., Broy, M., Zamulin, A.V. (eds.) PSI 1999. LNCS, vol. 1755, pp. 62\u201379. Springer, Heidelberg (2000)"},{"key":"16_CR25","unstructured":"Klyuchnikov, I.: Supercompiler HOSC 1.0: Under the Hood. Preprint 63, KIAM, Moscow (2009). http:\/\/library.keldysh.ru\/preprint.asp?id=2009-63"},{"key":"16_CR26","doi-asserted-by":"crossref","unstructured":"Bolingbroke, M., Peyton Jones, S.: Supercompilation by evaluation. In: Proceedings of the Third ACM Haskell Symposium on Haskell, pp. 135\u2013146. ACM (2010)","DOI":"10.1145\/2088456.1863540"},{"key":"16_CR27","unstructured":"Klimov, A., Romanenko, S. (eds.) Third International Valentin Turchin Workshop on Metacomputation, Publishing House \u201cUniversity of Pereslavl\u201d, Russia (2012)"},{"key":"16_CR28","unstructured":"Nemytykh, A. (ed.) Second International Valentin Turchin Memorial Workshop on Metacomputation, Publishing House \u201cUniversity of Pereslavl\u201d, Russia (2010)"}],"container-title":["Lecture Notes in Computer Science","Perspectives of System Informatics"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-662-46823-4_16","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,2,15]],"date-time":"2023-02-15T07:25:36Z","timestamp":1676445936000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-662-46823-4_16"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783662468227","9783662468234"],"references-count":28,"URL":"https:\/\/doi.org\/10.1007\/978-3-662-46823-4_16","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015]]},"assertion":[{"value":"19 April 2015","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}