Is Impredicativity Implicitly Implicit? - Stefan Monnier; Nathaniel Bos (TYPES, 2019)

Lassie: HOL4 tactics by example. - Heiko Becker; Nathaniel Bos; Ivan Gavran; Eva Darulova; Rupak Majumdar (CPP, 2021)