Sound and Complete Elimination of Singleton Kinds

Abstract

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.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Jan 01, 2000
Accession Number
ADA375894

Entities

People

  • Karl Crary

Organizations

  • Carnegie Mellon University

Tags

DTIC Thesaurus Topics

  • Abstracts
  • Algorithms
  • Assembly Languages
  • Calculus
  • Compilers
  • Computer Science
  • Construction
  • Elimination
  • Erasure
  • Judgment
  • Language
  • New Jersey
  • Specifications
  • Standards
  • Symmetry
  • Test And Evaluation
  • Translations

Readers

  • Computational Linguistics
  • Theoretical Analysis.