Michael Backes, Catalin Hritcu, Thorsten Tarrach: Automatically Verifying Typing Constraints for a Data Processing Language. CPP 2011: 296-313