1991 | ReviewPaper | Buchkapitel
Singleton, union and intersection types for program extraction
verfasst von : Susumu Hayashi
Erschienen in: Theoretical Aspects of Computer Software
Verlag: Springer Berlin Heidelberg
Enthalten in: Professional Book Archive
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
Two type theories, ATT and ATTT, are introduced. ATT is an impredicative type theory closely related to the polymorphic type theory of implicit typing of MacQueen et al. [MPS86]. ATTT is another version of ATT that extends the Girard-Reynolds second order lambda calculus. ATT has notions of intersection, union and singleton types. ATTT has a notion of refinement types as in the type system for ML by Freeman and Pfenning [FP91], plus intersection and union of refinement types and singleton refinement types. We will show how singleton, union and intersection types serve for development of programs without unnecessary codes via a variant of the Curry-Howard isomorphism. More exactly, they give a way to write types as specifications of programs without unnecessary codes which is inevitable in the usual Curry-Howard isomorphism.