¶Abstract

The design space for concatenative programming languages, also known as stack-based programming languages, is largely under-explored. Most formal investigations of higher-order stack-based languages are done in the functional setting, requiring a cumbersome and unnecessary encoding. This dissertation describes a core programming language that captures the essence of the concatenative paradigm, provides a reduction semantics for this language, and introduces a sound type system. It also presents a sound and complete type inference algorithm. We expect that this model will serve as a starting point for future explorations of the concatenative language design space.