Do you have space for dessert? a verified space cost semantics for CakeML programs. - Alejandro Gómez-Londoño; Johannes Åman Pohjola; Hira Taqdees Syeda; Magnus O. Myreen; Yong Kiam Tan (Proc. ACM Program. Lang., 2020)

A flat reachability-based measure for CakeML's cost semantics. - Alejandro Gómez-Londoño; Magnus O. Myreen (IFL, 2021)

Hood-Melville Queue. - Alejandro Gómez-Londoño (Arch. Formal Proofs, 2021)

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)