- CompCertTSO, a version of CompCert for multithreaded execution with a weak memory model by Peter Sewell's group.
- A short description from J Strother Moore's web pages.
- J Strother Moore: Piton, a mechanically verified assembly-level language, 1996. DOI:10.1007/978-0-585-33654-1
- J Strother Moore: A mechanically verified language implementation, 1989. DOI:10.1007/BF00243133
- Computational Logic's technical reports, in particular #22 and #30 on Piton (the latter appears to be the tech report version of the 1989 paper) and #37 on a Gypsy to Piton code generator.