We show that the extensional ordering of the sequential functionals of pure type 3, e.g. as defined via game semantics [2, 4], is not cpo-enriched. ws that this model does not equ...
Based on natural deduction, Pure Type Systems (PTS) can express a wide range of type theories. In order to express proof-search in such theories, we introduce the Pure Type Sequent...