From Higher-Order Logics to Programming Verified by Coq