Devine, Michel Patrick (1984) A program verifier for total correctness based on intuitionistic type theory. Masters thesis, Concordia University.