A constructive type theory for simple imperative programming

by Kevin Robert Charter, University of Alberta. Dept. of Computing Science