SDPE との関係: HOAS

Higher-Order Abstract Syntax

[Pfenning & Elliott 88]:

object level の binding をmeta level の binding であらわす

例：

?x. ?y. (x @ y) ? ?(?a. ?(?b. (a @ b)))

Previous slide

Next slide

Back to first slide

View graphic version