Proving correctness of modular functional programs. - Christopher Owens (1999)