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 http://homotopytypetheory.org/book/. 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

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!