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.
Archive for the ‘intuitionism’ Category
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.