Archive for the ‘intuitionism’ Category

Quiet Nights and Quiet Stars

Six month retrospective on thinking small. I describe work optimizing GHC backend like LLVM, conversion of Paul Tarau’s bijective Godel numbering to term algebras in regular shape polymorphic parallel arrays library. I note Vladimir Veovodsky’s interest in Martin-Lof Type theory. And Agda as a potential target implementation for univalent foundations in mathematics.

A Winter of Philosophy and Logic

Winter was a time of deep contemplation and thoughtful reflection. I describe my readings in intuitionistic logic, type theory and the open source tooling that allows me to get my hands dirty and stay free.