Singleton, Union, and Intersection Types for Program Extraction

Two types 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. ((1986), Inform. and Control 71, 95-130). 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 ((1991), in "ACM SIGPLAN ′91, " ACM Press), 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 the unnecessary codes which are inevitable in the usual Curry-Howard isomorphism.

Authors

• S. Hayashi

Keywords

No keywords are indexed for this paper.