The Completeness of Typing for Context-Semantics

• Autorzy: Coquand T.
• Języki publikacji: EN

Abstrakty

EN

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

EN

Hindley's completeness theorem

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2007
• Tom: Vol. 77, nr 4
• Strony: 293--301
• Opis fizyczny: bibliogr. 16 poz.

Twórcy

autor

Coquand T.

• Department of Computer Science, Chalmers University of Technology, Göteberg,,

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