A Verified Generational Garbage Collector for CakeML. - Adam Sandberg Ericsson; Magnus O. Myreen; Johannes Åman Pohjola (J. Autom. Reason., 2019)