{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,1]],"date-time":"2026-04-01T15:01:54Z","timestamp":1775055714942,"version":"3.50.1"},"reference-count":21,"publisher":"Pleiades Publishing Ltd","issue":"3","license":[{"start":{"date-parts":[[2015,5,1]],"date-time":"2015-05-01T00:00:00Z","timestamp":1430438400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2015,5,1]],"date-time":"2015-05-01T00:00:00Z","timestamp":1430438400000},"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":["Program Comput Soft"],"published-print":{"date-parts":[[2015,5]]},"DOI":"10.1134\/s0361768815030068","type":"journal-article","created":{"date-parts":[[2015,5,28]],"date-time":"2015-05-28T09:40:22Z","timestamp":1432806022000},"page":"170-182","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Supercompilation for Martin-Lof\u2019s type theory"],"prefix":"10.1134","volume":"41","author":[{"given":"I. G.","family":"Klyuchnikov","sequence":"first","affiliation":[]},{"given":"S. A.","family":"Romanenko","sequence":"additional","affiliation":[]}],"member":"137","published-online":{"date-parts":[[2015,5,29]]},"reference":[{"issue":"3","key":"6258_CR1","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. Programming Languages Systems (TOPLAS), 1986, vol. 8, no. 3, pp. 292\u2013325.","journal-title":"ACM Trans. Programming Languages Systems (TOPLAS)"},{"key":"6258_CR2","volume-title":"The Language Refal: The Theory of Compilation and Metasystem Analysis","author":"VF Turchin","year":"1980","unstructured":"Turchin, V.F., The Language Refal: The Theory of Compilation and Metasystem Analysis, New York University Press, 1980."},{"issue":"1","key":"6258_CR3","doi-asserted-by":"publisher","first-page":"14","DOI":"10.1134\/S0361768807010033","volume":"33","author":"A Lisitsa","year":"2007","unstructured":"Lisitsa, A. and Nemytykh, A., Verification as a parameterized testing (experiments with the scp4 supercompiler), Program. Comput. Software, 2007, vol. 33, no. 1, pp. 14\u201323.","journal-title":"Program. Comput. Software"},{"key":"6258_CR4","volume-title":"Proc. 3rd International Valentin Turchin Workshop on Metacomputation","author":"AV Klimov","year":"2012","unstructured":"Klimov, A.V., Klyuchnikov, I.G., and Romanenko, S.A., Automatic verification of counter systems via domainspecific multiresult supercompilation, Proc. 3rd International Valentin Turchin Workshop on Metacomputation, Klimov, A. and Romanenko, S., Eds. (Pereslavl-Zalessky, 2012), Pereslavl: Univ. of Pereslavl Press, 2012."},{"key":"6258_CR5","volume-title":"Proc. 7th International Andrei Ershov Memorial Conference (PSI 2009)","author":"IG Klyuchnikov","year":"2009","unstructured":"Klyuchnikov, I.G. and Romanenko, S.A., Proving the equivalence of higher-order terms by means of supercompilation, Proc. 7th International Andrei Ershov Memorial Conference (PSI 2009), Pnueli, A., Virbitskaite, I., and Voronkov, A., Eds., Novosibirsk, 2009."},{"key":"6258_CR6","volume-title":"Cand. Sci. Dissertation","author":"I Klyuchnikov","year":"2010","unstructured":"Klyuchnikov, I., Inferring and proving properties of functional programs by means of supercompilation, Cand. Sci. Dissertation, Moscow: Keldysh Institute of Applied Mathematics, 2010."},{"key":"6258_CR7","doi-asserted-by":"crossref","first-page":"249","DOI":"10.1007\/3-540-62064-8_21","volume":"1181","author":"AP Nemytykh","year":"1996","unstructured":"Nemytykh, A.P. and Pinchuk, V.A., Program transformation with metasystem transitions: experiments with a supercompiler, in Perspectives of System Informatics, 1996, vol. 1181, pp. 249\u2013260.","journal-title":"Perspectives of System Informatics"},{"key":"6258_CR8","doi-asserted-by":"crossref","unstructured":"Turchin, V.F., Supercompilation: techniques and results, in Perspectives of System Informatics, 1996, vol. 1181.","DOI":"10.1007\/3-540-62064-8_20"},{"key":"6258_CR9","volume-title":"Proc. 3rd International Valentin Turchin Workshop on Metacomputation","author":"I Klyuchnikov","year":"2012","unstructured":"Klyuchnikov, I. and Romanenko, S., Towards higherlevel supercompilation, Proc. 3rd International Valentin Turchin Workshop on Metacomputation, Klimov, A. and Romanenko, S., Eds., (Pereslavl-Zalessky, 2012), Pereslavl: Univ. of Pereslavl Press, 2012."},{"key":"6258_CR10","volume-title":"Preprint of Keldysh Inst. Appl. Math., Russ. Acad. Sci.","author":"I Klyuchnikov","year":"2010","unstructured":"Klyuchnikov, I., Supercompiler HOSC: Proof of correctness, Preprint of Keldysh Inst. Appl. Math., Russ. Acad. Sci., Moscow, 2010. http:\/\/library.keldysh.ru\/preprint.asp?id=2010-31."},{"key":"6258_CR11","volume-title":"Proc. 2nd International Valentin Turchin Memorial Workshop on Metacomputation","author":"D Krustev","year":"2010","unstructured":"Krustev, D., A simple supercompiler formally verified in Coq, Proc. 2nd International Valentin Turchin Memorial Workshop on Metacomputation, Nemytykh, A.P., Ed. (Pereslavl-Zalessky, 2010), Pereslavl: Univ. of Pereslavl Press, 2010."},{"key":"6258_CR12","volume-title":"Proc. Workshop on Proof-Search in Typetheoretic Languages (CADE-12)","author":"A Pardo","year":"1994","unstructured":"Pardo, A. and da Rosa, S., Program transformation in Martin-Lof\u2019s type theory, Proc. Workshop on Proof-Search in Typetheoretic Languages (CADE-12), 1994."},{"key":"6258_CR13","volume-title":"Programming in Martin-Lof\u2019s Type Theory","author":"B Nordstroom","year":"1990","unstructured":"Nordstroom, B., Petersson, K., and Smith, J.M., Programming in Martin-Lof\u2019s Type Theory, Oxford University Press, 1990."},{"key":"6258_CR14","volume-title":"Type Theory and Functional Programming","author":"S Thompson","year":"1991","unstructured":"Thompson, S., Type Theory and Functional Programming, Redwood City: Addison Wesley Longman, 1991."},{"key":"6258_CR15","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, 2012."},{"key":"6258_CR16","doi-asserted-by":"publisher","first-page":"355","DOI":"10.1017\/S0956796899003500","volume":"9","author":"G Hutton","year":"1999","unstructured":"Hutton, G., A tutorial on the universality and expressiveness of fold, J. Funct. Program., 1999, vol. 9, pp. 355\u2013372.","journal-title":"J. Funct. Program."},{"key":"6258_CR17","doi-asserted-by":"publisher","first-page":"197","DOI":"10.1007\/3-540-45842-5_13","volume-title":"Types for Proofs and Programs","author":"C McBride","year":"2002","unstructured":"McBride, C., Elimination with a motive, in Types for Proofs and Programs, Berlin: Springer, 2002, pp. 197\u2013216"},{"key":"6258_CR18","first-page":"1001","volume":"21","author":"A Loh","year":"2010","unstructured":"Loh, A., McBride, C., and Swierstra, W., A tutorial implementation of a dependently typed lambda calculus, Fundamenta Informaticae, 2010, vol. 21, pp. 1001\u20131032.","journal-title":"Fundamenta Informaticae"},{"key":"6258_CR19","volume-title":"Preprint of Keldysh Inst. Appl. Math., Russ. Acad. Sci.","author":"IG Klyuchnikov","year":"2011","unstructured":"Klyuchnikov, I.G. and Romanenko, S.A., MRSC: a toolkit for building multi-result supercompilers, Preprint of Keldysh Inst. Appl. Math., Russ. Acad. Sci., Moscow, 2011. http:\/\/library.keldysh.ru\/preprint.asp?lg=e&id=2011-77."},{"key":"6258_CR20","volume-title":"Preprint of Keldysh Inst. Appl. Math., Russ. Acad. Sci.","author":"I Klyuchnikov","year":"2009","unstructured":"Klyuchnikov, I., Supercompiler HOSC 1.0: Under the hood, Preprint of Keldysh Inst. Appl. Math., Russ. Acad. Sci., Moscow, 2009. http:\/\/library.keldysh.ru\/preprint.asp?id=2009-63."},{"key":"6258_CR21","volume-title":"Proc. 3rd International Valentin Turchin Workshop on Metacomputation","year":"2012","unstructured":"Proc. 3rd International Valentin Turchin Workshop on Metacomputation, Klimov, A. and Romanenko, S., Eds. (Pereslavl-Zalessky, 2012), Pereslavl: Univ. of Pereslavl Press, 2012."}],"container-title":["Programming and Computer Software"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1134\/S0361768815030068.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1134\/S0361768815030068","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1134\/S0361768815030068","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1134\/S0361768815030068.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,4,1]],"date-time":"2026-04-01T02:20:36Z","timestamp":1775010036000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1134\/S0361768815030068"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015,5]]},"references-count":21,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2015,5]]}},"alternative-id":["6258"],"URL":"https:\/\/doi.org\/10.1134\/s0361768815030068","relation":{},"ISSN":["0361-7688","1608-3261"],"issn-type":[{"value":"0361-7688","type":"print"},{"value":"1608-3261","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015,5]]},"assertion":[{"value":"1 December 2014","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"29 May 2015","order":2,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}