A Theory of Typed Hygienic Macros, a dissertation by
Dave Herman
We present the lambda_m-calculus, a semantics for a language of hygienic macros
with a non-trivial theory. Unlike Scheme, where programs must be macro-expanded
to be analyzed, our semantics admits reasoning about programs
as they appear to programmers. Our contributions include a semantics of
hygienic macro expansion, a formal definition of α-equivalence that is independent
of expansion, and a proof that expansion preserves α-equivalence.
The key technical component of our language is a type system similar to
Culpepper and Felleisen's "shape types," but with the novel contribution of
binding signature types, which specify the bindings and scope of a macro’s
arguments.
Recent comments
16 weeks 2 days ago
16 weeks 2 days ago
16 weeks 2 days ago
38 weeks 3 days ago
42 weeks 5 days ago
44 weeks 2 days ago
44 weeks 2 days ago
47 weeks 15 hours ago
51 weeks 4 days ago
51 weeks 5 days ago