Trustworthy Systems

Singleton : A general-purpose dependently-typed assembly language

Authors

Simon Winwood and Manuel Chakravarty

NICTA

UNSW

Abstract

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.

BibTeX Entry

  @inproceedings{Winwood_Chakravarty_11,
    address          = {Austin, Texas, USA},
    author           = {Winwood, Simon and Chakravarty, Manuel},
    booktitle        = {The Sixth ACM SIGPLAN Workshop on Types in Language Design and Implementation},
    isbn             = {978-1-4503-0484-9},
    month            = jan,
    pages            = {3--14},
    paperurl         = {https://trustworthy.systems/publications/nicta_full_text/4366.pdf},
    publisher        = {ACM},
    title            = {Singleton : A general-purpose dependently-typed assembly language},
    year             = {2011}
  }

Download