March 7th, 2007

beartato phd

(no subject)

Went to a talk by Ed Fredkin, explaining his blue-sky dreams about revolutionizing transportation systems, which kind of left me in a bummed mood, for the talk was vague, confusing, and generally kind of disappointingly not as full of promising ideas as the posters so seductively advertised. Afterwards hung out for a while at Kiva Han downing hot tea and chatting with Karen, which contrarily was quite pleasant.

I am making some progress understanding a tech report by Adam Poswolsky, one of Carsten Schürmann's students, which explains how they are using temporal logic to do functional programming over higher-order data. It's extremely unhygienic from a judgmental-dogma standpoint; lots of context operators that peer into the types of hypotheses 'nnat. I'm trying to keep an open mind despite its superficial heresies. I really want to believe that all that's essentially going on with higher-order data is a type recursion operator μ at kind N → T where N is the kind of finite types (e.g. void, unit, bool, etc.) and T is the kind of all types.