Lecture dates

NOT COVERED THIS YEAR - WON'T BE EXAMINED !!! 
We only briefly discussed dependent types in the last lecture (14.5.), the materials here are intended only for those who are interested in learning more.

Reading

Programming in IDRIS: A Tutorial [PDF]

Read Section 3. Types and Functions

A. Bove, P. Dybjer: Dependent Types at work. [PDF]

Additional material

Read the materials explaining how to simulate dependent types in Haskell using GADTs, type families etc. in Lecture VIII.