Dependent types are a wonderful way to construct correct functional programming and specify interfaces as Edwin has shown in his nice book on type driven development using a welsh dragon. But shall we go further in the esoteric world of homotopy type theory? I will try to motivate this and I am looking forward to some discussions with people who have a more pragmatic attitude to dependent types.
- When: 25th May 2018 11:00 - 12:30
- Where: Cole 1.33a
- Format: Seminar