Archive for the ‘haskell’ Category

Values, Types and Foundations

Recaps my Values, Types and Foundations talk at the OMG September Technical Meeting. Describes the computational, logic and philosophical presentation topics. Describes the demonstrations based on Oleg Kiselov and Anton Setzer’s work in Haskell and Agda. Constrasts the approach with ISO 24707 Common Logic.

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.

I Love it When a Plan Comes Together

Luckily a year ago I made a good choice in programming languages: Haskell. Language trends are harder to read. Think there’s a practical use for Second order Lambda Calculus with Polymorphism? I do. Category theory is embedded in the core libraries of the language which makes incorporating information flow and the logical environment of the Information Flow Framework a natural fit.