Caires, L, Seco JC.  2012.  Working note on a type-checking algorithm for BST. : CITI / DI-FCT-UNL