TY - JOUR AU - Haeusler , Edward Hermann AU - Pereira , Luiz Carlos Pinheiro Dias PY - 1999/10/31 Y2 - 2024/03/29 TI - The rules-as types interpretations of Schröder-Heister's extension of natural deduction JF - Manuscrito: Revista Internacional de Filosofia JA - Manuscrito - Rev. Int. Fil. VL - 22 IS - 2 SE - Artigos DO - UR - https://periodicos.sbu.unicamp.br/ojs/index.php/manuscrito/article/view/8666391 SP - 149-163 AB - <p>From this theorem we can conclude that any Cartesian Closed Category with finite co-products is a model λR. The addition of types of arbitrary levels does not interfere with the basic semantical intuitions. The enlarged expressive power of λR relies, for exemple, on the possibility of considering certain assumption formation processes as the specification of programming modules (as in MODULA- II (Wirth (1985))): the modules hide their implementations, but specify the interface (types of the premises, of the discharged hypothesis ando f the conclusion) that they ought to have with the world.</p> ER -