Kalas: A Verified, End-To-End Compiler for a Choreographic Language. - Johannes Åman Pohjola; Alejandro Gómez-Londoño; James Shaker; Michael Norrish (ITP, 2022)