User loginNavigation |
Have your AHOS and eat HOAS too!Noam (uid 3913) announced on his weblog at the beginning of the year a technique that allows one to bridge the gap between meta-theoretic notions of function space and theory-internal notions, in a way that is compatible with structural induction over Higher-Order Abstract Syntax, by applying Reynolds' Definitional Interpreters for Higher-Order Programming Languages [pdf] (cf. LtU classic), and realised it as an implementation in Twelf. That's a lot of ideas in one sentence, but since HOAS is in the air this month, I guess there are a good number of LtUers who will want to get to grips with this stuff. Refs:
|
Browse archives
Active forum topics
|
Recent comments
16 weeks 18 hours ago
20 weeks 2 days ago
21 weeks 6 days ago
21 weeks 6 days ago
24 weeks 4 days ago
29 weeks 2 days ago
29 weeks 2 days ago
29 weeks 5 days ago
29 weeks 5 days ago
32 weeks 3 days ago