Title: A constructive type theory for simple imperative programming