Singleton: 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 abstraction, generalised singleton types allow strong statements to be made about the functional behaviour of Singleton programs. We have formalised basic properties of Singleton's type system, namely type safety and a type erasure property, using the Coq proof assistant.