DAT350 / DIT235 Types for programs and proofs