Homer: A Higher-Order Observational Equivalence Model checkER. - David Hopkins 002; C.-H. Luke Ong (CAV, 2009)

A Fragment of ML Decidable by Visibly Pushdown Automata. - David Hopkins 002; Andrzej S. Murawski; C.-H. Luke Ong (ICALP (2), 2011)

Hector: An Equivalence Checker for a Higher-Order Fragment of ML. - David Hopkins 002; Andrzej S. Murawski; C.-H. Luke Ong (CAV, 2012)

Fragments of ML Decidable by Nested Data Class Memory Automata. - Conrad Cotton-Barratt; David Hopkins 002; Andrzej S. Murawski; C.-H. Luke Ong (FoSSaCS, 2015)