Contest phase 1 is over. Running the ICFP contest has been a blast so far; I recommend that you all do it. I was very worried everyone would hate the game, or we'd get no submissions, or whatever, but nothing seriously bad seems to have happened other than (1) a team discovering a degenerate strategy as a result of a dumb last-minute addition we made to the game board and (2) a few tempers flaring over some OS-specific problems (there's a nasty intermittent bug with pipes in Windows that people were getting angry about, apparently).
Now there's just the huge, daunting task of evaluating the submissions, coupled with the huger, daunting-er task of doing this whole thing again, faster.
Bob Harper gave a talk today, and I missed it due to class. He was talking about Twelf; I really wish I'd seen it, Twelf looks like it might be immediately applicable to my work but I can't figure out exactly how it works from glancing over the tutorial.
Now there's just the huge, daunting task of evaluating the submissions, coupled with the huger, daunting-er task of doing this whole thing again, faster.
Bob Harper gave a talk today, and I missed it due to class. He was talking about Twelf; I really wish I'd seen it, Twelf looks like it might be immediately applicable to my work but I can't figure out exactly how it works from glancing over the tutorial.
posted by Jacob Matthews at
18:44
1 Comments:
Wow, he gets around! He was the keynote on Friday at NEPLS. The talk was interesting, although he was a bit bellicose about the competition. He boasted that his group are the only ones to achieve the PoplMark challenge and that they did it in a week.
I have to say I'm a little skeptical about two things in Twelf:
1) I still feel like theorem-proving via types in Curry-Howard is cutesy and ultimately really weird;
and more substantively,
2) the use of HOAS requires a lot of weird hacks for modeling variables that require anything beyond substitution--these hacks were the brunt of the technical portion of the talk.
As for the difficulty of using Twelf, I haven't gotten through much of the tutorial, but he claimed that Greg Morrissett picked it up quickly (albeit after trading some emails with the authors) and was very positive about his experience so far. Of course, saying that something is easy for Greg Morrissett is probably not saying very much. :)
Without having used Twelf, I'd guess the biggest hurdles in understanding it are:
1) understanding the purpose of the meta-language vs. the object-languages;
2) understanding the HOAS representation of bindings in the object-language via bindings in the meta-language;
3) understanding the use of Curry-Howard to formulate all judgments as types.
By
Dave Herman, at 00:19
Post a Comment
<< Home