How Generic is a Generic Black End? Using MLRISC as a Black End for the TIL Compiler. - Andrew Bernard; Robert Harper 001; Peter Lee 001 (Types in Compilation, 1998)

Temporal Logic for Proof-Carrying Code. - Andrew Bernard; Peter Lee 001 (CADE, 2002)