Game semantics based equivalence checking of higher-order programs. - David G. B. Hopkins (2012)