Monday, May 03, 2010

A Theory of Typed Hygienic Macros

A Theory of Typed Hygienic Macros
PhD Dissertation, 2010

We present the λ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.

8 comments:

Jonathan said...

Congratulations Dave. When is your defence?

Matt said...

"We"?

Dave Herman said...

@Jonathan: done.

@Matt: Leave us alone. We are royalty. Our committee never mentioned this, and it is too late for us to change it anyway.

David said...

If you hadn't said 'we', we would have definitely heard of that from the committee!

Gregg said...

Congratulations!

Noel said...

Congratulations!

Lindsey Kuper said...

Congratulations!

goatstrangler said...

Could you post a single-spaced version? It looks great as-is, but printing any part would take a whole tree. :)