Type Checking with Universes

by: Robert Harper, Robert Pollack

Theoretical Computer Science, Vol. 89, No. 1. (1991), pp. 107-136.

View FullText article

CiteSeer (at Penn State), CiteSeer (at MIT), CiteSeer (at Zurich), CiteSeer (at Singapore)

Reviews [Write a review of this article]

There are no reviews of this article

Find related articles from these CiteULike users

huitseeker

Find related articles with these CiteULike tags

polymorphism, type, universe

Abstract

Various formulations of constructive type theories have been proposed to serve as the basis for machine-assisted proof and as a theoretical basis for studying programming languages. Many of these calculi include a cumulative hierarchy of "universes," each a type of types closed under a collection of type-forming operations. Universes are of interest for a variety of reasons, some philosophical (predicative vs. impredicative type theories), some theoretical (limitations on the closure...

@article{citeulike:3032630, abstract = {Various formulations of constructive type theories have been proposed to serve as the basis for machine-assisted proof and as a theoretical basis for studying programming languages. Many of these calculi include a cumulative hierarchy of \"universes,\" each a type of types closed under a collection of type-forming operations. Universes are of interest for a variety of reasons, some philosophical (predicative vs. impredicative type theories), some theoretical (limitations on the closure...}, author = {Harper, Robert and Pollack, Robert }, citeulike-article-id = {3032630}, journal = {Theoretical Computer Science}, keywords = {polymorphism, type, universe}, number = {1}, pages = {107--136}, posted-at = {2008-07-22 13:18:30}, priority = {3}, title = {Type Checking with Universes}, url = {http://citeseer.ist.psu.edu/harper91type.html}, volume = {89}, year = {1991} }

RIS record

TY - JOUR ID - citeulike:3032630 L3 - citeulike-article-id:3032630 TI - Type Checking with Universes JF - Theoretical Computer Science VL - 89 IS - 1 SP - 107 EP - 136 N2 - Various formulations of constructive type theories have been proposed to serve as the basis for machine-assisted proof and as a theoretical basis for studying programming languages. Many of these calculi include a cumulative hierarchy of "universes," each a type of types closed under a collection of type-forming operations. Universes are of interest for a variety of reasons, some philosophical (predicative vs. impredicative type theories), some theoretical (limitations on the closure... KW - polymorphism KW - type KW - universe AU - Harper, Robert AU - Pollack, Robert PY - 1991/// UR - http://citeseer.ist.psu.edu/harper91type.html ER -

RIS BibTeX