DAT350 / DIT233 Types for programs and proofs