Banner Portal
The rules-as types interpretations of Schröder-Heister's extension of natural deduction
v. 22 n. 2 (1999), Artigos
v. 22 n. 2 (1999)

The rules-as types interpretations of Schröder-Heister's extension of natural deduction

Artigos
Publicado 1999-10-31
Edward Hermann Haeusler
Catholic University of Rio de Janeiro
https://orcid.org/0000-0002-4999-7476
Luiz Carlos Pinheiro Dias Pereira
Catholic University of Rio de Janeiro
PDF

Palavras-chave

Dedução natural
Schröder-Heister

Como 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 Filosofia, 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: 18 abr. 2024.
ACM ACS APA ABNT Chicago Harvard IEEE MLA Turabian Vancouver

Baixar Citação

Endnote/Zotero/Mendeley (RIS) BibTeX

Resumo

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

Referências

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
Este trabalho está licenciado sob uma licença Creative Commons Attribution 4.0 International License.

Copyright (c) 1999 https://creativecommons.org/licenses/by/4.0/

Downloads

Não há dados estatísticos.