Why Homotopy type Theory (HoTT) matters – Professor Thorsten Altenkirch

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.

Event details

  • When: 25th May 2018 11:00 - 12:30
  • Where: Cole 1.33a
  • Format: Seminar