I am collecting various links that I found interesting. This includes blogs that I read from time to time, cool posts that facinate me, etc. I am trying to keep this categorised, but it does go out of hands sometimes.

Blogs

• Jesper Cockx writes all kind of things about Agda.
• Ayberk Tosun works with Martin Escardo on the intersection of topology and type theory.
• Andeas Abel one of the key Agda developers.
• Guillaume Allais writes about type theory, Agda, Idris, etc.
• Francesco Mazzoli — all kinds of computer science topics.
• Amélia Liao writes about Cubical Agda and type theory.
• Martín Escardó writes about type theory and mathematics.
• Andrej Bauer writes about mathematics and type theory.
• András Kovács writes about type theory, often from the implementor’s perspective.
• Siddharth Bhat writes about all kinds of CS topics.
• Tai-Danae Bradley writes about category theory and mathematics.
• Conor’s blog explains constructions that float around in his head.
• Peter Hancock does not blog a lot, but the stuff that is there is quite interesting. A number of his papers and documents are available here.

Interesting articles

• Seemingly impossible function explores how to find an infinite sequence of binary digits that corresponds to the given predicate (in finite time)!
• dreamtt is a toy implementation of bidirectional elaborator.
• Elaboration Zoo is a collection of experiments that Andras did when studying how to write efficient elaborators.
• MicroKanren in J describes an implementation of relational language MiniKanren in J.

Agda-related

• 1lab is a web page about Cubical Agda with a lot of examples.

Books

• The Dao of Functional Programming by Bartosz Milewski.
• Topology from the perspective of category theory.
• Modern C talks about some interesting modern features of C.
• The Tao of Tmux is a book about tmux.

Research

• Conference Deadline Calendar. This is a very nice idea, given that it will be updated.

• Proving compiler correctness is a course by Xavier Leroy with a number of interesting implementational details. This is somewhat super-reduced version of CompCert.

• Realizability by Andrej Bauer. There is also a link to GitHub repo with more details.

• n-Category Café group blog about physics math and philosophy.

Non-technical

• Artteritory is a web portal about art.
• Alexander Piatigorsky a web page about the philosopher with his works etc.
• Gorky media [ru] is a web portal about literature.
• Rigas Laiks is a journal about culture and philosophy.
• Нож [ru] is a web portal about culture.