Ilya Klyuchnikov
(Илья Григорьевич Ключников)

Projects

• FABA - fast bytecode analysis
• A supercompiler for Martin-Löf's type theory
• A Multi-Result Supercompiler
• A Higher-Order Supercompiler
• A Small Positive Supercompiler in Scala

Publications

• Ilya Klyuchnikov. Inference of @NotNull annotations from java bytecode. RSDN Magazine (in Russian) link
• Sergei Grechanik, Ilya Klyuchnikov, and Sergei Romanenko. Staged Multi-Result Supercompilation: Filtering by Transformation. Meta2014. pdf
• Ilya Klyuchnikov. Nullness Analysis of Java Bytecode via Supercompilation over Abstract Values. Meta2014. pdf
• Ilya Klyuchnikov and Sergei Romanenko. Certifying supercompilation for Martin-Löf's type theory. PSI14. preprint pdf
• Ilya Klyuchnikov and Sergei Romanenko. TT Lite: a supercompiler for Martin-Löf's type theory. Preprint. Keldysh Institute of Applied Mathematics, Moscow. 2013. pdf
• Sergei A. Grechanik, Ilya G. Klyuchnikov, Sergei A. Romanenko. Staged multi-result supercompilation: filtering before producing. Keldysh Institute Preprints, (70), 2013. - 28 p. link PDF
• Andrei Klimov, Ilya Klyuchnikov and Sergei Romanenko. Implementing a domain-specific multi-result supercompiler by means of the MRSC toolkit. Preprint 24. Keldysh Institute of Applied Mathematics, Moscow. 2012. pdf
• И.Г. Ключников, С.А. Романенко. Суперкомпиляция высшего уровня как путь к метасистемному переходу. - Программирование №5, 2012, с.35-53.
• Andrei Klimov, Ilya Klyuchnikov and Sergei Romanenko. Automatic verification of counter systems via domain-specific multi-result supercompilation. Preprint 19. Keldysh Institute of Applied Mathematics, Moscow. 2012. pdf
• Ilya Klyuchnikov and Sergei Romanenko. MRSC: a toolkit for building multi-result supercompilers. Preprint 77. Keldysh Institute of Applied Mathematics, Moscow. 2011. pdf
• Ilya Klyuchnikov and Sergei A. Romanenko. Higher-level supercompilation as a metasystem transition. Programming and Computer Software, September 2012, Volume 38, Issue 5, pp 231-244 DOI
• Ilya Klyuchnikov and Sergei A. Romanenko. Multi-result supercompilation as branching growth of the penultimate level in metasystem transitions. In Proceedings of the 8th international conference on Perspectives of System Informatics (PSI'11), Edmund Clarke, Irina Virbitskaite, and Andrei Voronkov (Eds.). Lecture Notes in Computer Science, volume 7162, pages 210-226. Springer-Verlag, Berlin, Heidelberg, 2012. (ISBN: 978-3-642-29708-3) DOI=10.1007/978-3-642-29709-0_19 DOI
• Ilya Klyuchnikov. The ideas and methods of supercompilation. Practice of Functional Programming, 7, 2011. In Russian.
  Илья Ключников. Суперкомпиляция: идеи и методы // Практика функционального программирования, №7, 2011.
• Ilya Klyuchnikov. Towards effective two-level supercompilation. Preprint 81. Keldysh Institute of Applied Mathematics, Moscow. 2010. pdf
• Ilya Klyuchnikov. Supercompiler HOSC 1.5: homeomorphic embedding and generalization in a higher-order setting. Preprint 62. Keldysh Institute of Applied Mathematics, Moscow. 2010. pdf
  (Russian version: pdf)
• Ilya Klyuchnikov. "Inferring and proving properties of functional programs by means of supercompilation". PhD Thesis [In Russian]:
  Выявление и доказательство свойств функциональных программ методами суперкомпиляции // Диссертация, Авторефереат
• Ilya Klyuchnikov. Higher-order supercompilation. [In Russian]:
  И.Г. Ключников. Суперкомпиляция функций высших порядков // Программные системы: теория и приложения: электрон. научн. журн. 2010. № 3(3), с. 37–71. pdf, link
• Ilya Klyuchnikov. Supercompiler HOSC: proof of correctness. Preprint 31. Keldysh Institute of Applied Mathematics, Moscow. 2010. pdf
  (Russian translation: pdf)
• Ilya Klyuchnikov and Sergei Romanenko. Towards Higher-Level Supercompilation. In: Second International Workshop on Metacomputation in Russia. 2010. pdf
• Ilya Klyuchnikov. Supercompiler HOSC 1.1: proof of termination. Preprint 21. Keldysh Institute of Applied Mathematics, Moscow. 2010. pdf
  (Russian translation: pdf)
• Ilya Klyuchnikov. Supercompiler HOSC 1.0: under the hood. Preprint 63. Keldysh Institute of Applied Mathematics, Moscow, 2009. pdf
  (Russian translation: pdf)
• Ilya Klyuchnikov and Sergei Romanenko. Proving the Equivalence of Higher-Order Terms by Means of Supercompilation. In: Proceedings of the Seventh International Andrei Ershov Memorial Conference: Perspectives of System Informatics. LNCS 5947. 2009. pdf DOI
• Ilya Klyuchnikov and Sergei Romanenko. SPSC: a Simple Supercompiler in Scala. In: International Workshop on Program Understanding 19-23 June, Altai Mountains, Russia. 2009. pdf
• Ilya Klyuchnikov and Sergei Romanenko. SPSC: a Supercompiler in Scala. [In Russian]:
  Илья Ключников, Сергей Романенко. SPSC: Суперкомпилятор на языке Scala. // Программные продукты и системы. 2009. №2 (86). pdf

Slides

• Introduction to Metacomputaion (Presented at sssev2011). Joint work with Sergei Abramov:
  • Metacomputation. A Gentle Introduction (pptx)
  • Metacomputation. A Gentle Introduction to Advanced Topics (pdf)
• Multi-Result Supercompilation as Branching Growth of the Penultimate Level in Metasystem Transitions. Talk at PSI-2011, 29 June 2011 pdf
• Multi-Result Supercompilation as Branching Growth of the Penultimate Level in Metasystem Transitions. Talk at Turchin's 80 anniversary, 14 Feb 2011 [In Russian] pdf
• Supercompiler HOSC: the rationale behind the algorithms // 2010 August. [In Russian] pdf
• Towards Higher-Level Supercompilation // 2010 July, Meta-2010. pdf
• Proving the Equivalence of Higher-Order Terms by Means of Supercompilation (PSI'09) pdf
• SPSC: a Simple Supercompiler in Scala (PU'09) pdf

Background

I'm a graduate of applied mathematics and physics from Moscow Institute of Physics and Technology, Department of Aeromechanics and Flying Engineering, Aircraft Ballistics, Aerodynamics and Control chair.

2007-2010: Postgraduate student at M.V.Keldysh Institute of Applied Mathematics, the Russian Academy of Sciences, Moscow.

2010, November: Ph.D., Mathematics and physics, M.V.Keldysh Institute of Applied Mathematics, the Russian Academy of Sciences, Moscow. Thesis: "Inferring and proving properties of functional programs by means of supercompilation"

2010-now: Researcher, M.V.Keldysh Institute of Applied Mathematics, the Russian Academy of Sciences, Moscow