hosc-docs

HOSC: A Higher-Order Supercompiler in Scala

This site is associated with the project https://github.com/ilya-klyuchnikov/hosc.

A supercompiler is a program transformer that traces the possible generalized histories of computation by the source program, and builds an equivalent target program, whose structure is, in a sense, “simpler” than the structure of the source program. The simplification is achieved by removing certain “redundant” actions from the source program.

The goal of the project is to implement in Scala a positive supercompiler that is able to deal with higher-order functions.

The current version of hosc can be run as a command-line application or as a web-application.

hosc deals with programs written in a simple lazy functional language with higher-order functions. The intended operational semantics of the language is normal-order graph reduction to weak head normal form.

News

2010, December I.G. Klyuchnikov. Towards effective two-level supercompilation. Preprint 81. Keldysh Institute of Applied Mathematics, Moscow. 2010. pdf

2010, November 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 (in Russian: pdf)

2010, November Ilya Klyuchnikov. “Inferring and proving properties of functional programs by means of supercompilation”. PhD Thesis (In Russian): Выявление и доказательство свойств функциональных программ методами суперкомпиляции // Диссертация, Авторефереат

2010, September Ilya Klyuchnikov. Higher-order supercompilation. (In Russian): И.Г. Ключников. Суперкомпиляция функций высших порядков // Программные системы: теория и приложения: электрон. научн. журн. 2010. № 3(3), с. 37–71. pdf, link

2010, July Ilya Klyuchnikov and Sergei Romanenko. Towards Higher-Level Supercompilation. In Proceedings of the Second International Workshop on Metacomputation in Russia. Pereslavl-Zalessky, Russia, July 1-5, 2010. PDF link

2010, June I.G. Klyuchnikov. Supercompiler HOSC: proof of correctness. Preprint 31, Keldysh Institute of Applied Mathematics, Moscow, 2010. PDF link (Also available in russian: PDF_ru )

2010, April I.G. Klyuchnikov. Supercompiler HOSC 1.1: proof of termination. Preprint 21, Keldysh Institute of Applied Mathematics, Moscow, 2010. PDF link

2010, January HLL is extended with non-exhaustive patterns Simple example

2009, December I.G.Klyuchnikov. Supercompiler HOSC 1.0: under the hood. Preprint 63, Keldysh Institute of Applied Mathematics, Moscow, 2009. PDF link

2009, June Ilya Klyuchnikov and Sergei Romanenko. Proving the Equivalence of Higher-Order Terms by Means of Supercompilation. In: Perspectives of Systems Informatics (Proceedings of Seventh International Andrei Ershov Memorial Conference, PSI 2009, Novosibirsk, Russia, June 15-19, 2009). Novosibirsk: A.P. Ershov Institute of Informatics Systems, 2009, pages 150-158. PDF slides PDF

Documentation