Supercompiler HOSC 1.1: proof of termination

Ilya Klyuchnikov. Supercompiler HOSC 1.1: proof of termination. Preprint 21, Keldysh Institute of Applied Mathematics, Moscow, 2010.

Abstract

The paper contributes the proof of termination of an experimental supercompiler HOSC dealing with higher-order functions.