Title: Machine-supported reasoning about functional language programs and implementations