Higher Assurance Functional RDF in Haskell describes the results of my recent code writing project. The purpose of the project is to demonstrate each of the capabilities suggested by the title above in a working solution and to develop a set of practices to deliver such a solution.
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.
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.