You may not like Tait's Method, but you've got to admit ...
It seems like everything I'm learning these days is coming from unpublished books. For a long time I was reading stuff from Felleisen and Flatt's Programming Languages and Lambda Calculi (google for it); from it I got a foothold on contextual equivalence after quite a bit of struggling. Then, more recently, I discovered Bob Harper's Type Systems for Programming Languages (available from his homepage), which has a great amount of good material and also talks about contextual equivalence in a totally different way from Felleisen and Flatt. (For instance see his discussion of "ciu-equivalence".)
Anyway. Sorry for the lack of updates. Strangely, the more I'm doing the less I can write about, and I've been very busy lately. I've been doing a tremendous amount on my multi-language semantics project recently and I'd love to talk about all of it, but unfortunately all of it is a bit too fresh for me to talk about it here.
What I can do, though, is take this opportunity to publicly praise Derek Dreyer's advanced type theory class for directly helping the research I'm working on now. Derek's class is the first class in which I had to understand the proof that the simply-typed lambda-calculus terminates; I learned how to do that proof about six weeks ago, and this afternoon I adapted it to complete the proof of a very surprising multi-language systems result. Imagine that! Things that I learn in school being relevant to research!
Anyway. Sorry for the lack of updates. Strangely, the more I'm doing the less I can write about, and I've been very busy lately. I've been doing a tremendous amount on my multi-language semantics project recently and I'd love to talk about all of it, but unfortunately all of it is a bit too fresh for me to talk about it here.
What I can do, though, is take this opportunity to publicly praise Derek Dreyer's advanced type theory class for directly helping the research I'm working on now. Derek's class is the first class in which I had to understand the proof that the simply-typed lambda-calculus terminates; I learned how to do that proof about six weeks ago, and this afternoon I adapted it to complete the proof of a very surprising multi-language systems result. Imagine that! Things that I learn in school being relevant to research!
posted by Jacob Matthews at
00:50
4 Comments:
Hm, a subject line aimed at PL researchers who know about logical relations and listen to The Mountain Goats. Or, in other words, me.
By
Dave Herman, at 21:17
When you say you can't write about what you're doing, is it because the work it has yet to be published? And if so, what worries you about writing about work before it is published? Are you too busy, or do you think others will steal your ideas? I'm curious, because I don't think the later is a very good reason.
By
Noel, at 03:59
Dave: wow, I was pretty much expecting that the subject-line would be sort of a one-person in-joke to myself. Glad someone else caught it :)
Noel: no, nothing to do with keeping secrets, I'm just too busy to write down coherent chunks of what I'm doing; and also I'm working on the back half of my multi-language paper right now and I'm not sure I can explain what's going on there without explaining the entire front half first.
That said I did come up with something a couple days ago that's relevant to PLT Schemers who use contracts and doesn't require any knowledge of the multi-language stuff. If it turns out to work I'll write it up here.
By
Jacob Matthews, at 09:58
That felleisen/flatt monograph turned into the Redex book: http://redex.racket-lang.org/sewpr-preface.html
By
Robby Findler, at 20:49
Post a Comment
<< Home