E-ccc: Between ccc and topos (Q1117018)

The cartesian closed category (ccc) and topos differ in both descriptive power and executability. The ccc cannot express the concept of subtypes, while it has the executable structure as a model of typed \(\lambda\)- calculus. On the other hand, the topos has strong expressive power of subtypes, although it does not in general have a good correspondence to any computation system. This paper introduces the structure of e-ccc, as an intermediate of the ccc and topos. The e-ccc has the correspondence to the \(\lambda\)-calculus based on an extended abstract data type theory and thus can be considered to be executable. Moreover, relations between e- ccc and ccc or topos are discussed. In particular, the topos is proved to be a specially-structured e-ccc.