Course Design and Tool Development for Functional Programming Integrating with Program Verification: from the Perspective of the Interactive Theorem Prover. - Haipeng Qu; Yaojun Hou; Rongqian Zhou (ACM TUR-C, 2023)