http://www.doc.ic.ac.uk/~jpw48
This is an unofficial reimagining of the Archive of Formal Proofs
Syntax and semantics of a GPU kernel programming languageby John Wickerson
Ribbon Proofsby John Wickerson