A general-purpose dependently-typed assembly language
Simon Winwood · UNSWorks (UNSW Sydney) · 2022
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