Sound and Complete Elimination of Singleton Kinds

Karl Crary

To appear at ACM SIGPLAN Workshop on Types in Compilation (TIC00), Montreal, Canada, 21 September 2000


Singleton kinds provide an elegant device for expressing type equality information resulting from modern module languages, but they can 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.

Server START Conference Manager
Update Time 27 Jul 2000 at 15:10:31
Start Conference Manager
Conference Systems