Sound and Complete Elimination of Singleton Kinds

9 years 10 months ago
Sound and Complete Elimination of Singleton Kinds
Singleton kinds provide an elegant device for expressing type equality information resulting from modern module languages, but they can severely complicate the metatheory of languages in which they appear. I present a translation from a language with singleton kinds to one without, and prove that translation to be sound and complete. This translation is useful for type-preserving compilers generating typed target languages. The proof of soundness and completeness is done by normalizing type equivalence derivations using Stone and Harper's type equivalence decision procedure. This research was sponsored by the Advanced Research Projects Agency CSTO under the title The Fox Project: Advanced Languages for Systems Software", ARPA Order No. C533, issued by ESC ENS under Contract No. F19628-95-C-0050. The views and conclusions contained in this document are those of the authors and should not be interpreted as representing o cial policies, either expressed or implied, of the Defen...
Karl Crary
Added 25 Aug 2010
Updated 25 Aug 2010
Type Conference
Year 2000
Where TIC
Authors Karl Crary
Comments (0)