A Note on Forcing and Type Theory

• Autorzy: Coquand T. , Jaber G.
• Języki publikacji: EN

Abstrakty

EN

The goal of this note is to show the uniform continuity of definable functional in intuitionistic type theory as an application of forcing with dependent type theory.

Słowa kluczowe

EN

type theory; dependent types; forcing

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2010
• Tom: Vol. 100, nr 1/4
• Strony: 43--52
• Opis fizyczny: Bibliogr. 14 poz.

Twórcy

autor

Coquand T.

autor

Jaber G.

• Computer Science Department, Gothenburg University, S 412 96 Göteborg, Sweden,

Bibliografia

• [1] S. Allen. A Non-Type-TheoreticDefinition ofMartin-Löf's Types. Proceedings of the Second IEE Symposium LICS 1987, 215-224.
• [2] H. Barendregt. The impact of the lambda calculus. Bulletin of Symbolic Logic, Volume 3, 1997, 181-215.
• [3] M.J. Beeson. Foundations of Constructive Mathematics. Springer-Verlag, 1985.
• [4] E.W. Beth. The foundations of mathematics. North-Holland, Amsterdam, 1965.
• [5] L.E.J. Brouwer. über Definitionsbereiche von Funktionen. Mathematische Annalen, 97:60-75. English translation in van Heijenoort, (1967, 446-463).
• [6] P. Cohen. The discovery of forcing. Rocky Mountain J. Math. 32 (2002), 1071-110.
• [7] K. Gödel. On a hitherto unexploited extension of the finitary standpoint. in Collected Works, Vol. II. Publications 1938-1974, Oxford University Press, 1990.
• [8] D. Hilbert. über das Unendliche. Mathematische Annalen, 95:161-190. Lecture given in Münster, 4 june 1925. English translation in van Heijenoort, (1967, 367-392).
• [9] J.L. Krivine. Structures de réalisabilité, RAM et ultrafiltre sur N. To appear, 2010.
• [10] P. Martin-Löf. On the strength of intuitionistic reasoning. Unpublished report, talk at the Bucharest conference, 1971.
• [11] P.Martin-Löf. An intuitionistic theory of types in Twenty-Five Years of Type Theory, G. Sambin and J. Smith Eds., Oxford University Press, 1998 (reprinted version of an unpublished report from 1972).
• [12] R. Platek. Generalized Recursion Theory, Stanford and Me. In: Odifreddi, P. (ed.) Kreiseliana, About and Around Georg Kreisel (1996).
• [13] W.W. Tait. Intensional interpretations of functional of finite types I. Journal of Symbolic Logic 32 (1967), 198-212.
• [14] J. van Heijenoort (ed.) From Frege to Hilbert: A Source Book in Mathematical Logic, 1897-1941. Harvard University Press, 1967.