Keywords
Schröder-Heister
How to Cite
Abstract
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.
References
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).
This work is licensed under a Creative Commons Attribution 4.0 International License.
Copyright (c) 1999 https://creativecommons.org/licenses/by/4.0/
Downloads
