{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T21:27:14Z","timestamp":1725571634729},"publisher-location":"Berlin, Heidelberg","reference-count":19,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540255932"},{"type":"electronic","value":"9783540320142"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2005]]},"DOI":"10.1007\/11417170_1","type":"book-chapter","created":{"date-parts":[[2010,12,16]],"date-time":"2010-12-16T19:29:35Z","timestamp":1292527775000},"page":"1-9","source":"Crossref","is-referenced-by-count":1,"title":["Completeness Theorems and \u03bb-Calculus"],"prefix":"10.1007","author":[{"given":"Thierry","family":"Coquand","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"1_CR1","unstructured":"Aehlig, K.: On Fragments of Analysis with Strengths of Finitely Iterated Inductive Definitions. PhD thesis, Munich (2003)"},{"key":"1_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"22","DOI":"10.1007\/3-540-45413-6_6","volume-title":"Typed Lambda Calculi and Applications","author":"T. Altenkirch","year":"2001","unstructured":"Altenkirch, T., Coquand, T.: A finitary subsystem of the polymorphic \u03bb-calculus. In: Abramsky, S. (ed.) TLCA 2001. LNCS, vol.\u00a02044, pp. 22\u201328. Springer, Heidelberg (2001)"},{"key":"1_CR3","series-title":"Lecture Notes in Mathematics","doi-asserted-by":"crossref","DOI":"10.1007\/BFb0091894","volume-title":"Iterated inductive definitions and subsystems of analysis: recent proof-theoretical studies","author":"W. Buchholz","year":"1981","unstructured":"Buchholz, W., Feferman, S., Pohlers, W., Sieg, W.: Iterated inductive definitions and subsystems of analysis: recent proof-theoretical studies. Lecture Notes in Mathematics, vol.\u00a0897. Springer, Berlin (1981)"},{"key":"1_CR4","unstructured":"Buchholz, W., Sch\u00fctte, K.: Proof theory of impredicative subsystems of analysis. In: Studies in Proof Theory, Monographs, Bibliopolis, Naples, vol.\u00a02 (1988)"},{"key":"1_CR5","first-page":"34","volume":"4","author":"K. G\u00f6del","year":"1933","unstructured":"G\u00f6del, K.: Zur intuitionistischen Arithmetik und Zahlentheorie. Ergebnisse einers math. Koll., Heft\u00a04, 34\u201338 (1933)","journal-title":"Ergebnisse einers math. Koll., Heft"},{"issue":"1-2","key":"1_CR6","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0304-3975(83)90136-6","volume":"22","author":"R. Hindley","year":"1983","unstructured":"Hindley, R.: The completeness theorem for typing \u03bb-terms. Theoret. Comput. Sci.\u00a022(1-2), 1\u201317 (1983)","journal-title":"Theoret. Comput. Sci."},{"key":"1_CR7","doi-asserted-by":"crossref","unstructured":"Hindley, R.: Basic simple type theory. In: Cambridge Tracts in Theoretical Computer Science, vol.\u00a042. Cambridge University Press, Cambridge (1997)","DOI":"10.1017\/CBO9780511608865"},{"key":"1_CR8","doi-asserted-by":"publisher","first-page":"241","DOI":"10.2307\/2964281","volume":"23","author":"P. Lorenzen","year":"1958","unstructured":"Lorenzen, P.: Logical reflection and formalism. J. Symb. Logic\u00a023, 241\u2013249 (1958)","journal-title":"J. Symb. Logic"},{"key":"1_CR9","doi-asserted-by":"publisher","first-page":"81","DOI":"10.2307\/2266681","volume":"16","author":"P. Lorenzen","year":"1951","unstructured":"Lorenzen, P.: Algebraische und logistische Untersuchungen \u00fcber freie Verb\u00e4nde. J. Symbolic Logic\u00a016, 81\u2013106 (1951)","journal-title":"J. Symbolic Logic"},{"key":"1_CR10","unstructured":"Martin-L\u00f6f, P.: Notes on constructive mathematics. In: Almquist and Wixsekk, Stockholm (1968)"},{"key":"1_CR11","first-page":"93","volume":"24","author":"P. Martin-L\u00f6f","year":"1972","unstructured":"Martin-L\u00f6f, P.: Infinite terms and a system of natural deduction. Compositio Math.\u00a024, 93\u2013103 (1972)","journal-title":"Compositio Math."},{"key":"1_CR12","series-title":"Synthese Lib.","doi-asserted-by":"crossref","first-page":"343","DOI":"10.1007\/978-94-010-0526-5_16","volume-title":"Logic, meaning and computation","author":"P. Martin-L\u00f6f","year":"2001","unstructured":"Martin-L\u00f6f, P.: A construction of the provable wellorderings of the theory of species. In: Logic, meaning and computation. Synthese Lib., vol.\u00a0305, pp. 343\u2013351. Kluwer Academic Publishers, Dordrecht (2001)"},{"issue":"3","key":"1_CR13","first-page":"353","volume":"12","author":"P. Novikov","year":"1943","unstructured":"Novikov, P.: On the consistency of a certain logical calculus. Matematicesky sbovnik\u00a012(3), 353\u2013369 (1943)","journal-title":"Matematicesky sbovnik"},{"issue":"1","key":"1_CR14","doi-asserted-by":"publisher","first-page":"33","DOI":"10.2307\/2275175","volume":"57","author":"A. Pitts","year":"1992","unstructured":"Pitts, A.: On an interpretation of second-order quantification in first-order intuitionistic propositional logic. J. Symbolic Logic\u00a057(1), 33\u201352 (1992)","journal-title":"J. Symbolic Logic"},{"key":"1_CR15","unstructured":"Poincar\u00e9, H.: La logique de l\u2019infini. In: Revue de metaphysique et de morale (1909)"},{"key":"1_CR16","unstructured":"Russell, B., Whitehead, A.: Principia Mathematica, Cambridge, pp. 1910\u20131913"},{"key":"1_CR17","doi-asserted-by":"publisher","first-page":"249","DOI":"10.2969\/jmsj\/00730249","volume":"7","author":"G. Takeuti","year":"1955","unstructured":"Takeuti, G.: On the fundamental conjecture of GLC. I. J. Math. Soc. Japan\u00a07, 249\u2013275 (1955)","journal-title":"J. Math. Soc. Japan"},{"issue":"2","key":"1_CR18","doi-asserted-by":"publisher","first-page":"299","DOI":"10.2307\/1970691","volume":"86","author":"G. Takeuti","year":"1967","unstructured":"Takeuti, G.: Consistency proofs of subsystems of classical analysis. Ann. of Math.\u00a086(2), 299\u2013348 (1967)","journal-title":"Ann. of Math."},{"key":"1_CR19","unstructured":"Takeuti, I.: Proof of calculability through cut elimination. In: Proof theory and reverse mathematics, Kyoto, pp. 78\u201393 (1993)"}],"container-title":["Lecture Notes in Computer Science","Typed Lambda Calculi and Applications"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11417170_1.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T07:03:45Z","timestamp":1619507025000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11417170_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005]]},"ISBN":["9783540255932","9783540320142"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/11417170_1","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2005]]}}}