Alastair Donaldson and John Wickerson, together with their students and colleagues, have had three OOPSLA papers accepted for presentation at the SPLASH 2021 conference. This is one of the premier conferences in the field of research into Programming Languages, and is being held in a hybrid setting, both online and in Chicago. The first paper describes the first proven-correct tool for compiling software programs into hardware designs; the second paper describes an empirically validated model of how shared memory works on hybrid CPU/FPGA devices; and the third paper describes the results of an investigation into the forward-progress guarantees that modern GPU devices offer to programmers.