Pilsner: a compositionally verified compiler for a higher-order imperative language. - Georg Neis; Chung-Kil Hur; Jan-Oliver Kaiser; Craig McLaughlin; Derek Dreyer; Viktor Vafeiadis (ICFP, 2015)

Do be do be do. - Sam Lindley; Conor McBride; Craig McLaughlin (POPL, 2017)

Triangulating context lemmas. - Craig McLaughlin; James McKinna; Ian Stark (CPP, 2018)

Doo bee doo bee doo. - Lukas Convent; Sam Lindley; Conor McBride; Craig McLaughlin (J. Funct. Program., 2020)

Relational reasoning for effects and handlers. - Craig McLaughlin (2020)

Pancake: Verified Systems Programming Made Sweeter. - Johannes Åman Pohjola; Hira Taqdees Syeda; Miki Tanaka; Krishnan Winter; Tsun Wang Sau; Benjamin Nott; Tiana J. Tsang Ung; Craig McLaughlin; Remy Seassau; Magnus O. Myreen; Michael Norrish; Gernot Heiser (PLOS@SOSP, 2023)

Dargent: A Silver Bullet for Verified Data Layout Refinement. - Zilin Chen; Ambroise Lafont; Liam O'Connor; Gabriele Keller; Craig McLaughlin; Vincent Jackson; Christine Rizkallah (Proc. ACM Program. Lang., 2023)