We introduce Ultra S-types in Pure Type Systems generalizing earlier work on program extraction in Type Theory. This general and comprehensinve setting includes the work by Paulin based on realizability interpretations, Burstall and McKinna's Theory of Specification and Deliverables, Poll's Programming Logic, Severi and Szasz's Theory of Specifications. We show how to express all these theories as particular Pure Type Systems with the Ultra S-types. This general presentation helps understanding and comparing all this different approaches to program extraction.

Se presenta una extensión de los Sistemas de Tipos Puros puros con tipos Ultra-S, que generalizan los trabajos previos sobre extracción de programas en teoría de Tipos. Este marco general incluye los de Paulin basados en interpretación de realización, la teoría de Especificaciónes y Liberales de Burstall y Makinna, la lógica de programación de Poll, y la teoría de Especificaciónes de Severy y Szasz. Se muestra como expresar todas estas teorías como casos particulares de Sistemas de Tipos Puros con tipos Ultra-S. Esta presentación general permite una mejor comprensión y comparación de los diferentes enfoques existentes de la extracción de programas.