For those who want a good PL read, I can recommend Michael Arntzenius' PhD Thesis (available at 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?)

\(sort : \mathrm{list}\ \mathbb{R} \to \mathrm{list}\ \mathbb{R}\) is a computable function

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

hal.archives-ouvertes.fr/hal-0

If \(\mathrm{gcd}(a_1, \cdots, a_n) = 1\), then $$\frac{(a_1 + \cdots + a_n - 1)!}{a_1! \cdots a_n!}$$ is a whole number.

Do we have LaTeX here? $\det(\exp(A)) = \exp(\tr(A))$

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
types.pl

A Mastodon instance for programming language theorists and mathematicians. Or just anyone who wants to hang out.