We investigate possible extensions of arbitrary given Pure Type Systems with additional sorts and rules which preserve the normalization property. In particular we identify the following interesting extensions: the disjoint union of two PTSs and, the PTS which intuitively captures the " -logic of -terms" and poly which intuitively denotes the predicative polymorphism extension of. These results suggest a new approach to the study of the meta-theory of PTSs, by examination of the relationships between different calculi and predicative extensions which allow more expressiveness with equivalent logical strength. © 2014 Springer International Publishing Switzerland.
CITATION STYLE
Roux, C., & Van Doorn, F. (2014). The structural theory of pure type systems. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 8560 LNCS, pp. 364–378). Springer Verlag. https://doi.org/10.1007/978-3-319-08918-8_25
Mendeley helps you to discover research relevant for your work.