swMATH ID: 13320
Software Authors: David Hopkins , Andrzej S. Murawski , C.-H. Luke Ong
Description: HECTOR: an equivalence checker for a higher-order fragment of ML. We present Hector, an observational equivalence checker for a higher-order fragment of ML. The input language is RML, the canonical restriction of standard ML to ground-type references. Hector accepts programs from a decidable fragment of RML identified by us at ICALP’11, which comprises programs of short-type (order at most 2 and arity at most 1) that may contain free variables whose arguments are also of short-type. This is an expressive fragment that contains complex higher-order types, and includes many examples from the literature which have proven challenging to verify using other methods. To our knowledge, Hector is the first fully-automated equivalence checker for higher-order, call-by-value programs. Both sound and complete, the tool relies on the fully abstract game semantics of RML to construct, on-the-fly, visibly pushdown automata which precisely capture program behaviour. These automata are then checked for language equivalence, and if they are inequivalent a counterexample (in the form of a separating context) is constructed.
Homepage: http://link.springer.com/chapter/10.1007%2F978-3-642-31424-7_63
Related Software: HOMER; GTRECS2; C-SHORe; SLAM
Cited in: 1 Publication

Cited in 0 Serials

Citations by Year