Mechanized Metatheory for User-Defined Type Extensions
1st Informal ACM SIGPLAN Workshop on Mechanizing Metatheory (WMM 2006), Portland, Oregon, September 21, 2006.
Daniel Marino, Brian Chin, Todd Millstein, Gang Tan, Robert Simmons, David Walker
A one-page overview of our project to use the Twelf proof assistant as
a powerful framework for programmer-defined type-system extensions.
[PDF]