publications:
- title: "Supercompiler HOSC 1.5: homeomorphic embedding and generalization in a higher-order setting"
  author:
  - name: "Ilya Klyuchnikov"
    link: "http://pat.keldysh.ru/~ilya/"
  year: "2010"
  abstract: "The paper describes the algorithm of the supercompiler HOSC 1.5, an experimental specializer dealing with programs written in a higher-order functional language. The design decisions behind the algorithm are illustrated through a series of examples. Of particular interest are the decisions related to generalization and homeomorphic embedding of expressions with bound variables. "
  links:
    "keldysh.ru": "http://library.keldysh.ru/preprint.asp?lg=e&id=2010-62"
  tags:
  - "programming languages"
  - "functional programming"
  - "language design"
  - "design"
  researchr: "https://researchr.org/publication/Klyuchnikov2010Hosc15"
  cites: 0
  citedby: 0
  institution: "Keldysh Institute of Applied Mathematics"
  type: "Preprint"
  number: "62"
  address: "Moscow"
  kind: "techreport"
  key: "Klyuchnikov2010Hosc15"
- title: "Supercompiler HOSC 1.0: under the hood"
  author:
  - name: "Ilya Klyuchnikov"
    link: "http://pat.keldysh.ru/~ilya/"
  year: "2009"
  abstract: "The paper describes the internal structure of HOSC, an experimental supercompiler dealing with programs written in a higher-order functional language. A detailed and formal account is given of the concepts and algorithms the supercompiler is based upon. "
  links:
    "keldysh.ru": "http://library.keldysh.ru/preprint.asp?lg=e&id=2009-63"
  tags:
  - "programming languages"
  - "rule-based"
  - "functional programming"
  researchr: "https://researchr.org/publication/Klyuchnikov2009HOSC"
  cites: 0
  citedby: 0
  institution: "Keldysh Institute of Applied Mathematics"
  type: "Preprint"
  number: "63"
  address: "Moscow"
  kind: "techreport"
  key: "Klyuchnikov2009HOSC"
- title: "Towards effective two-level supercompilation"
  author:
  - name: "Ilya Klyuchnikov"
    link: "http://pat.keldysh.ru/~ilya/"
  year: "2010"
  abstract: "The paper presents a number of improvements to the method of two-level supercompilation: a fast technique of lemma discovering by analyzing the expressions in the partial process tree, an enhancement to the algorithm of checking improvement lemmas based on the normalization of tick annotations, and a few techniques of finding simplified versions of lemmas discovered in the process of two-level supercompilation. "
  links:
    "keldysh.ru": "http://library.keldysh.ru/preprint.asp?lg=e&id=2010-81"
  tags:
  - "rule-based"
  researchr: "https://researchr.org/publication/Klyuchnikov2010Fast"
  cites: 0
  citedby: 0
  institution: "Keldysh Institute of Applied Mathematics"
  type: "Preprint"
  number: "81"
  address: "Moscow"
  kind: "techreport"
  key: "Klyuchnikov2010Fast"
- title: "Supercompiler HOSC 1.1: proof of termination"
  author:
  - name: "Ilya Klyuchnikov"
    link: "http://pat.keldysh.ru/~ilya/"
  year: "2010"
  abstract: "The paper contributes the proof of termination of an experimental supercompiler HOSC dealing with higher-order functions. "
  links:
    "keldysh.ru": "http://library.keldysh.ru/preprint.asp?lg=e&id=2010-21"
  tags:
  - "termination"
  researchr: "https://researchr.org/publication/Klyuchnikov2010HoscTermination"
  cites: 0
  citedby: 0
  institution: "Keldysh Institute of Applied Mathematics"
  type: "Preprint"
  number: "21"
  address: "Moscow"
  kind: "techreport"
  key: "Klyuchnikov2010HoscTermination"
- title: "Proving the Equivalence of Higher-Order Terms by Means of Supercompilation"
  author:
  - name: "Ilya Klyuchnikov"
    link: "http://pat.keldysh.ru/~ilya/"
  - name: "Sergei A. Romanenko"
    link: "http://pat.keldysh.ru/~roman/"
  year: "2009"
  doi: "http://dx.doi.org/10.1007/978-3-642-11486-1_17"
  abstract: "One of the applications of supercompilation is proving properties of programs. We focus in this paper on a specific task: proving term equivalence for a higher-order lazy functional language. The “classical” way to prove equivalence of two terms t1 and t2 is to write an equality function equals and to simplify the term (equals t1 t2). However, this works only when certain conditions are met. The paper presents another approach to proving term equivalence by means of supercompilation. In this approach we supercompile both terms and compare supercompiled terms syntactically. Some applications of the technique are discussed. In particular, one of these applications may lead to the development of a more powerful “higher-level” supercompiler. "
  links:
    doi: "http://dx.doi.org/10.1007/978-3-642-11486-1_17"
  tags:
  - "laziness"
  - "programming languages"
  - "functional programming"
  - "systematic-approach"
  - "domain-specific language"
  researchr: "https://researchr.org/publication/KlyuchnikovR09"
  cites: 0
  citedby: 0
  pages: "193-205"
  booktitle: "Perspectives of Systems Informatics, 7th International Andrei Ershov Memorial Conference, PSI 2009, Novosibirsk, Russia, June 15-19, 2009. Revised Papers"
  editor:
  - name: "Amir Pnueli"
    link: "https://researchr.org/alias/amir-pnueli"
  - name: "Irina Virbitskaite"
    link: "https://researchr.org/alias/irina-virbitskaite"
  - name: "Andrei Voronkov"
    link: "https://researchr.org/alias/andrei-voronkov"
  volume: "5947"
  series: "Lecture Notes in Computer Science"
  publisher: "Springer"
  isbn: "978-3-642-11485-4"
  kind: "inproceedings"
  key: "KlyuchnikovR09"
- title: "Supercompiler HOSC: proof of correctness"
  author:
  - name: "Ilya Klyuchnikov"
    link: "http://pat.keldysh.ru/~ilya/"
  year: "2010"
  abstract: "The paper presents the proof of correctness of an experimental supercompiler HOSC dealing with higher-order functions."
  links:
    "keldysh.ru": "http://library.keldysh.ru/preprint.asp?lg=e&id=2010-31"
  researchr: "https://researchr.org/publication/Klyuchnikov2010HoscCorrectness"
  cites: 0
  citedby: 0
  institution: "Keldysh Institute of Applied Mathematics"
  type: "Preprint"
  number: "31"
  address: "Moscow"
  kind: "techreport"
  key: "Klyuchnikov2010HoscCorrectness"