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.
Posts Tagged ‘Coquand’s Calculus of Constructions’
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.