Just Testing

Lambda Science
About Me

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.

My Other Sites
TwitterLinkedInTumblrScribd
Tags
Archive
2012 (5)
2011 (5)
2010 (14)
2009 (43)
2008 (30)
2007 (23)
Archive for

July 2010

 

First release of the CUDA backend for Accelerate

During the first Australian Haskell Hackathon, AusHac2010, we finally managed to complete the integration of the CUDA backend, written by Sean Lee and Trevor McDonell, into the array EDSL Accelerate.  It still doesn't cover the complete functionality of the current version of the Accelerate EDSL, but already allows for interesting GPU computations.  The package source (version 0.7.1.0) can be obtained from Hackage as usual.  There is now also a bug tracker.

Filed under  //  edsl   gpgpu   haskell   parallelism  
Posted
 

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.

Filed under  //  code certification   security   tal   types  
Posted
 

Haskell 2010 is complete!

The final version of the Haskell 2010 edition has been released: http://www.haskell.org/pipermail/haskell/2010-July/022189.html This completes my stewardship of the Haskell foreign function interface specification. It is now part of the language standard proper. The next language feature I personally like to see being integrated are type families, but that still requires much work.

Filed under  //  ffi   haskell   haskell2010  
Posted