Mechanized Metatheory for User-Defined Type Extensions
In 1st Informal ACM SIGPLAN Workshop on Mechanizing Metatheory
(WMM 2006), Portland, Oregon, September 21, 2006.
Daniel Marino, Brian Chin,
Todd Millstein,
Gang Tan,
Robert J. Simmons,
and
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]