Banner Portal
The rules-as types interpretations of Schröder-Heister's extension of natural deduction
PDF (Português (Brasil))

Palabras clave

Dedução natural
Schröder-Heister

Cómo citar

HAEUSLER , Edward Hermann; PEREIRA , Luiz Carlos Pinheiro Dias. The rules-as types interpretations of Schröder-Heister’s extension of natural deduction. Manuscrito: Revista Internacional de Filosofía, Campinas, SP, v. 22, n. 2, p. 149–163, 1999. Disponível em: https://periodicos.sbu.unicamp.br/ojs/index.php/manuscrito/article/view/8666391. Acesso em: 30 jun. 2024.

Resumen

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.

PDF (Português (Brasil))

Citas

Chi, W.H. (1991). Esquemas Abstratos para Dedução Natural Cálculo de Sequentes e λ-Calculus Tipado. Dissertação de Mestrado, Departamento de Informática, PUC-Rio.

Haeusler, E.H. & Pereira, L.C.P.D. (1992). A Denotational Semantics for Arbitrary Level Typed λ-Calculus, Monografias em Ciência da Computação (Departamento de Informática, PUC-RIO).

Poubel, H.W. & Pereira, L.C.P.D. (1993). A Categorical Approach to HIgher-Level Introduction and Elimination Rules, Reports in Mathematical Logic 27, pp. 3-19.

PRAWITZ, D. (1965). Natural Deduction. A Proof Theorical Study (Stockholm, Almqvist-Wiksell).

Schröder-Heister, P. (1984). A Natural Extension of Natural Deduction, Journal of Symbolic Logic, vol.49.

Wirth, N. (1985). Programming in Modula-2 (Berlin, Springer-Verlag).

Creative Commons License

Esta obra está bajo una licencia internacional Creative Commons Atribución 4.0.

Derechos de autor 1999 https://creativecommons.org/licenses/by/4.0/

Descargas

Los datos de descargas todavía no están disponibles.