Tytuł artykułu
Autorzy
Wybrane pełne teksty z tego czasopisma
Identyfikatory
Warianty tytułu
Języki publikacji
Abstrakty
We present a variation of Hindley's completeness theorem for simply typed [lambda]-calculus. It is based on a Kripke semantics where the worlds are contexts, called context-semantics. This variation was obtained indirectly by simplifying an analysis of a fragment of polymorphic [lambda]-calculus [2]. We relate in this way works done in proof theory [4,14] with a fundamental result in [lambda]-calculus.
Słowa kluczowe
Wydawca
Czasopismo
Rocznik
Tom
Strony
293--301
Opis fizyczny
bibliogr. 16 poz.
Twórcy
autor
- Department of Computer Science, Chalmers University of Technology, Göteberg,, coquand@cs.chalmers.se
Bibliografia
- [1] K. Aehlig. On Fragments of Analysis with Strengths of Finitely Iterated Inductive Definitions. PhD thesis, Munich, 2003.
- [2] Th. Altenkirch and Th. Coquand. A finitary subsystem of the polymorphic _-calculus. Typed lambda calculi and applications (Krak´ow, 2001), 22-28, Lecture Notes in Comput. Sci., 2044, Springer, Berlin, 2001.
- [3] H. Barendregt, M. Coppo and M. Dezani-Ciancaglini. A filter lambda model and the completeness of type assignment. J. Symbolic Logic 48 (1983), no. 4, 931-940 (1984).
- [4] W. Buchholz, S. Feferman,W. Pohlers andW. Sieg. Iterated inductive definitions and subsystems of analysis: recent proof-theoretical studies. Lecture Notes in Mathematics, 897. Springer-Verlag, Berlin-New York, 1981.
- [5] W. Buchholz, and K. Schütte. Proof theory of impredicative subsystems of analysis. Studies in Proof Theory. Monographs, 2. Bibliopolis, Naples, 1988.
- [6] S. Farkh and K. Nour. Un résultat de complétude pour les types 8+ du système F. C. R. Acad. Sci. Paris Sér. I Math. 326 (1998), no. 3, 275-279.
- [7] R. Hindley. The completeness theorem for typing _-terms. Theoret. Comput. Sci. 22 (1983), no. 1-2, 1-17.
- [8] R. Hindley. Basic simple type theory. Cambridge Tracts in Theoretical Computer Science, 42. Cambridge University Press, Cambridge, 1997.
- [9] P. Martin-Löf. A construction of the provable wellorderings of the theory of species. Logic, meaning and computation, 343-351, Synthese Lib., 305, Kluwer Acad. Publ., Dordrecht, 2001.
- [10] J.CMitchell and E.Moggi. Kripke-stylemodels for typed lambda calculus. Second Annual IEEE Symposium on Logic in Computer Science (Ithaca, NY, 1987). Ann. Pure Appl. Logic 51 (1991), no. 1-2, 99-124.
- [11] J.C. Reynolds. Towards a theory of type structure. Programming Symposium (Proc. Colloq. Programmation, Paris, 1974), pp. 408-425. Lecture Notes in Comput. Sci., Vol. 19, Springer, Berlin, 1974.
- [12] D. Scott. Open problem II 4 Lecture Notes in Computer Science, vol. 137, Springer-Verlag, 1982, p. 212-226.
- [13] G. Takeuti. On the fundamental conjecture of GLC. I. J. Math. Soc. Japan 7 (1955), 249-275.
- [14] G. Takeuti. Consistency proofs of subsystems of classical analysis. Ann. of Math. (2) 86 1967 299-348.
- [15] A. Troelstra. Intuitionistic formal systems. in Metamathematical investigation of intuitionistic arithmetic and analysis, pp. 1-96. Lecture Notes in Mathematics, Vol. 344, Springer, Berlin, 1973.
- [16] I. Takeuti. Proof of calculability through cut elimination. Proof theory and reverse mathematics (Kyoto, 1993), pp. 78-93
Typ dokumentu
Bibliografia
Identyfikator YADDA
bwmeta1.element.baztech-article-BUS5-0010-0012