For those who want a good PL read, I can recommend Michael Arntzenius' PhD Thesis (available at http://www.rntz.net/files/thesis.pdf ). The level of detail included in the wonderful narrative made it a really easy read (for me).

I don't even care very much about Datalog, but all the techniques deployed, in the manner they were deployed, captivated me.

(Not sure of rntz is on here?)

Oh very nice, looks like Pujet and Tabareau's paper on impredicative observational type theory is out! Excited to read this...

The 600-cell lives in 4 dimensions and has 120 vertices... but it's just the shadow of a more symmetrical shape in 8 dimensions that has twice as many vertices: 240 vertices!

It's called the 'E8 root polytope', and it's one of the most amazing structures in all of mathematics. Here is a picture of it projected down to the plane.

(By 'shadow', I mean you can project the E8 root polytope down to 4 dimensions and get the 600-cell.)

(3/n)

Show thread