Proof Assistants At the Hardware-Software Interface

POPL 2020