[Prev][Next][Index][Thread]
Paper announcement: Sound and Complete Elimination of Singleton Kinds
-
To: types@cis.upenn.edu
-
Subject: Paper announcement: Sound and Complete Elimination of Singleton Kinds
-
From: Karl Crary <crary@cs.cmu.edu>
-
Date: Mon, 10 Jan 2000 17:40:00 -0500
-
Importance: Normal
-
MMDF-Warning: Parse error in original version of preceding line at postoffice.srv.cs.cmu.edu
-
MMDF-Warning: Parse error in original version of preceding line at postoffice.srv.cs.cmu.edu
-
Reply-To: crary@cs.cmu.edu
I would like to announce the availability of the following paper at URL
http://www.cs.cmu.edu/~crary/papers/.
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.