A program verifier for total correctness based on intuitionistic type theory