Michael Y. Levin and Benjamin C. Pierce. TinkerType: A Language for Playing with Formal Systems. Journal of Functional Programming, 13(2), March 2003. A preliminary version appeared as an invited paper at the Logical Frameworks and Metalanguages Workshop (LFM), June 2000. [ bib | source code | full version | slides ]