Typing with Leftovers - A Mechanization of Intuitionistic Linear Logic Compilation The development has been typechecked with: Agda version 2.5.3 The Standard Library version 0.15
