¶Abstract

Stack based languages are widely used as byte-codes, as intermediate languages, and as programming languages for embedded devices. It is well-known how to check the types of simple stack-based languages such as for the Java virtual machine language, using Hindley-Milner type inference, or using Hoare logic. The simple Hindley-Milner type inference algorithm is insufficient to type-check higher order instructions, such as abstraction operators, in a stack-based language without annotations. This limitation occurs because we require first-class polymorphism. Our contribution is to describe a simple type-system and type-inference algorithm for higher-order instructions in a single stack stack-based language.