Abstract
The purpose of this note is to present a variation of Hindley’s completeness theorem for simply typed λ-calculus based on Kripke model. This variation was obtained indirectly by simplifying an analysis of a fragment of polymorphic λ-calculus [2].
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Aehlig, K.: On Fragments of Analysis with Strengths of Finitely Iterated Inductive Definitions. PhD thesis, Munich (2003)
Altenkirch, T., Coquand, T.: A finitary subsystem of the polymorphic λ-calculus. In: Abramsky, S. (ed.) TLCA 2001. LNCS, vol. 2044, pp. 22–28. Springer, Heidelberg (2001)
Buchholz, W., Feferman, S., Pohlers, W., Sieg, W.: Iterated inductive definitions and subsystems of analysis: recent proof-theoretical studies. Lecture Notes in Mathematics, vol. 897. Springer, Berlin (1981)
Buchholz, W., Schütte, K.: Proof theory of impredicative subsystems of analysis. In: Studies in Proof Theory, Monographs, Bibliopolis, Naples, vol. 2 (1988)
Gödel, K.: Zur intuitionistischen Arithmetik und Zahlentheorie. Ergebnisse einers math. Koll., Heft 4, 34–38 (1933)
Hindley, R.: The completeness theorem for typing λ-terms. Theoret. Comput. Sci. 22(1-2), 1–17 (1983)
Hindley, R.: Basic simple type theory. In: Cambridge Tracts in Theoretical Computer Science, vol. 42. Cambridge University Press, Cambridge (1997)
Lorenzen, P.: Logical reflection and formalism. J. Symb. Logic 23, 241–249 (1958)
Lorenzen, P.: Algebraische und logistische Untersuchungen über freie Verbände. J. Symbolic Logic 16, 81–106 (1951)
Martin-Löf, P.: Notes on constructive mathematics. In: Almquist and Wixsekk, Stockholm (1968)
Martin-Löf, P.: Infinite terms and a system of natural deduction. Compositio Math. 24, 93–103 (1972)
Martin-Löf, P.: A construction of the provable wellorderings of the theory of species. In: Logic, meaning and computation. Synthese Lib., vol. 305, pp. 343–351. Kluwer Academic Publishers, Dordrecht (2001)
Novikov, P.: On the consistency of a certain logical calculus. Matematicesky sbovnik 12(3), 353–369 (1943)
Pitts, A.: On an interpretation of second-order quantification in first-order intuitionistic propositional logic. J. Symbolic Logic 57(1), 33–52 (1992)
Poincaré, H.: La logique de l’infini. In: Revue de metaphysique et de morale (1909)
Russell, B., Whitehead, A.: Principia Mathematica, Cambridge, pp. 1910–1913
Takeuti, G.: On the fundamental conjecture of GLC. I. J. Math. Soc. Japan 7, 249–275 (1955)
Takeuti, G.: Consistency proofs of subsystems of classical analysis. Ann. of Math. 86(2), 299–348 (1967)
Takeuti, I.: Proof of calculability through cut elimination. In: Proof theory and reverse mathematics, Kyoto, pp. 78–93 (1993)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Coquand, T. (2005). Completeness Theorems and λ-Calculus. In: Urzyczyn, P. (eds) Typed Lambda Calculi and Applications. TLCA 2005. Lecture Notes in Computer Science, vol 3461. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11417170_1
Download citation
DOI: https://doi.org/10.1007/11417170_1
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-25593-2
Online ISBN: 978-3-540-32014-2
eBook Packages: Computer ScienceComputer Science (R0)