A General-Purpose Dependently-Typed Assembly Language

In this paper we present Singleton, a dependently typed assembly language. Based upon the calculus of inductive constructions, Singleton’s type system allows procedures abstracting over terms, types, propositions, and proof terms. Furthermore, Singleton includes generalised singleton types. In addition to the primitive singleton types of other languages, these generalised singleton types allow the values from arbitrary inductive types to be associated with the contents of registers and memory locations. Along with Singleton’s facility for term and proof