I research and teach programming languages, compilers, and their applications at the University of New South Wales (UNSW), Sydney. My main interest is in functional and parallel programming, and in particular, in Haskell.
My Twitter handle is TacticalGrace.
Check out my UNSW website.
Our paper Singleton: A General-Purpose Dependently-Typed Assembly Language will be presented at the ACM SIGPLAN Workshop on
Types in Language Design and Implementation (TLDI'11) co-located with POPL'11 in Austin, TX, in January. The final version of the paper is now available. See this previous post for some more information and proof scripts.
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.
