Paper announcement: Sound and Complete Elimination of Singleton Kinds

I would like to announce the availability of the following paper at URL

As always, comments or suggestions are most welcome.

	-- Karl Crary


Sounds and Complete Elimination of Singleton Kinds

Karl Crary

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.