Singleton: A general-purpose dependently-typed assembly language
In the paper Singleton: A general-purpose dependently-typed assembly language, we introduce Singleton, a typed assembly language that embeds a variant of the calculus of inductive constructions (CiC) as an assertion language in its type system. Moreover, Singleton procedures can abstract over propositions and proof terms. Singleton's name comes form its support for generalised singleton types that allow the values from arbitrary inductive types to be associated with the contents of registers and memory locations. Together these features allow strong statements to be made about the functional behaviour of Singleton programs.
Singleton's development was motivated by the desire for a typed assembly language that can establish high-level properties that are not implied by type safety alone, a requirement that we encountered in the context of runtime verification. For more details on that context, see our previous papers Secure Untrusted Binaries - Provably! and On the automated synthesis of proof-carrying temporal reference monitors.
Simon Winwood, on whose PhD work the paper is based, established basic properties of Singleton's type system, namely type safety and a type erasure property, using the Coq proof assistant: proof scripts.
