Log in

No account? Create an account
Notes from a Medium-Sized Island [entries|archive|friends|userinfo]

[ website | My Website ]
[ userinfo | livejournal userinfo ]
[ archive | journal archive ]

[Mar. 7th, 2007|05:44 pm]
[Tags|, , ]

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.

From: neelk
2007-03-07 11:09 pm (UTC)
I was under the impression that Adam had stopped using temporal logic. Are you looking at their newest (LICS '07) stuff?
(Reply) (Thread)
[User Picture]From: jcreed
2007-03-07 11:35 pm (UTC)
No, where is that?
(Reply) (Parent) (Thread)
From: neelk
2007-03-07 11:45 pm (UTC)
Try the Delphin web page. (Also, I made a mistake: it's been submitted, but I guess they haven't heard from the reviewers yet.)
(Reply) (Parent) (Thread)
[User Picture]From: gustavolacerda
2007-03-08 05:01 am (UTC)
Heh. I was so fascinated with Leitgeb's talk on informal provability (started at noon) that I decided to stay. Still, I decided to go down and say hello to Fredkin. He remembered me and gave a verbal answer to an email I sent him 4 years ago.

I should have told you about Leitgeb's talk (although Noam and Ruy were there). I can send you his slides... This is brand new work: very programmatic, not much worked out. So I fully intend to read his stuff, and discuss it with you.
(Reply) (Thread)