Category Archives: News

The HoTT book

The HoTT book is finished!

Since spring, and even before that, I have participated in a great collaborative effort on writing a book on Homotopy Type Theory. It is finally finished and ready for public consumption. You can get the book freely at Mike Shulman has written about the contents of the book, so I am not going to repeat that here. Instead, I would like to comment on the socio-technological aspects of making the book, and in particular about what we learned from open-source community about collaborative research.

Continue reading The HoTT book

A hott thesis

Egbert Rijke successfully defended his master thesis in Utrecht a couple of weeks ago. He published it on the Homotopy type theory blog (here is a direct link to the PDF file (revised)). The thesis is well written and it contains several new results, but most importantly, it is a gentle yet non-trivial introduction to homotopy type theory. If you are interested in the topic but do not know where to start, Egbert’s thesis might be perfect for you. As far as I know it is the first substantial piece of text written in (informal) homotopy type theory.

What I find most amazing about the work is that Egbert does not have to pretend to be a homotopy type theorist, like us old folks. His first contact with type theory was homotopy type theory, which impressed on his mind a new kind of geometric intuition about $\Pi$’s, $\Sigma$’s and $\mathrm{Id}$’s. If we perform enough such experiments on young bright students, strange things will happen.

Eff 3.0

Matija and I are pleased to announce a new major release of the eff programming language.

In the last year or so eff has matured considerably:

  • It now looks and feels like OCaml, so you won’t have to learn yet another syntax.
  • It has static typing with parametric polymorphism and type inference.
  • Eff now clearly separates three basic concepts: effect types, effect instances, and handlers.
  • How eff works is explained in our paper on Programming with Algebraic Effects and Handlers.
  • We moved the source code to GitHub, so go ahead and fork it!