Total Haskell is reasonable Coq.

Antal Spector-Zabusky, Joachim Breitner, Christine Rizkallah, Stephanie Weirich

Browse the full CPP paper archive.