{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T11:53:22Z","timestamp":1725537202497},"publisher-location":"Berlin, Heidelberg","reference-count":9,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642040269"},{"type":"electronic","value":"9783642040276"}],"license":[{"start":{"date-parts":[[2009,1,1]],"date-time":"2009-01-01T00:00:00Z","timestamp":1230768000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2009]]},"DOI":"10.1007\/978-3-642-04027-6_2","type":"book-chapter","created":{"date-parts":[[2009,9,14]],"date-time":"2009-09-14T13:27:52Z","timestamp":1252934872000},"page":"2-2","source":"Crossref","is-referenced-by-count":1,"title":["Forcing and Type Theory"],"prefix":"10.1007","author":[{"given":"Thierry","family":"Coquand","sequence":"first","affiliation":[]}],"member":"297","reference":[{"issue":"3","key":"2_CR1","doi-asserted-by":"publisher","first-page":"305","DOI":"10.2178\/bsl\/1102022660","volume":"10","author":"J. Avigad","year":"2004","unstructured":"Avigad, J.: Forcing in proof theory. Bulletin of Symbolic Logic\u00a010(3), 305\u2013333 (2004)","journal-title":"Bulletin of Symbolic Logic"},{"key":"2_CR2","volume-title":"Ergebnisse der Mathematik und ihrer Grenzgebiete (3) [Results in Mathematics and Related Areas (3)]","author":"M. Beeson","year":"1985","unstructured":"Beeson, M.: Foundations of constructive mathematics. Metamathematical studies. In: Ergebnisse der Mathematik und ihrer Grenzgebiete (3) [Results in Mathematics and Related Areas (3)], vol.\u00a06, Springer, Berlin (1985)"},{"issue":"2","key":"2_CR3","doi-asserted-by":"publisher","first-page":"600","DOI":"10.2307\/2586854","volume":"63","author":"S. Berardi","year":"1998","unstructured":"Berardi, S., Bezem, M., Coquand, T.: On the Computational Content of the Axiom of Choice. J. Symb. Log.\u00a063(2), 600\u2013622 (1998)","journal-title":"J. Symb. Log."},{"issue":"2","key":"2_CR4","doi-asserted-by":"publisher","first-page":"163","DOI":"10.1017\/S0960129506005093","volume":"16","author":"U. Berger","year":"2006","unstructured":"Berger, U., Oliva, P.: Modified bar recursion. Mathematical Structures in Computer Science\u00a016(2), 163\u2013183 (2006)","journal-title":"Mathematical Structures in Computer Science"},{"issue":"1","key":"2_CR5","doi-asserted-by":"publisher","first-page":"23","DOI":"10.2307\/2271946","volume":"43","author":"N. Goodman","year":"1978","unstructured":"Goodman, N.: Relativized realizability in intuitionistic arithmetic of all finite types. J. Symbolic Logic\u00a043(1), 23\u201344 (1978)","journal-title":"J. Symbolic Logic"},{"key":"2_CR6","doi-asserted-by":"publisher","first-page":"259","DOI":"10.1016\/S0304-3975(02)00776-4","volume":"308","author":"J.L. Krivine","year":"2003","unstructured":"Krivine, J.L.: Dependent choice, \u2018quote\u2019 and the clock. Th. Comp. Sc.\u00a0308, 259\u2013276 (2003)","journal-title":"Th. Comp. Sc."},{"key":"2_CR7","unstructured":"Krivine, J.L.: Structures de r\u00e9alisabilit\u00e9, RAM et ultrafiltre sur \u2115 (to appear, 2009)"},{"key":"2_CR8","series-title":"Stud. Logic Found. Math","doi-asserted-by":"crossref","first-page":"153","DOI":"10.1016\/S0049-237X(09)70189-2","volume-title":"Logic, methodology and philosophy of science, VI (Hannover, 1979)","author":"P. Martin-L\u00f6f","year":"1982","unstructured":"Martin-L\u00f6f, P.: Constructive mathematics and computer programming. In: Logic, methodology and philosophy of science, VI (Hannover, 1979). Stud. Logic Found. Math., vol.\u00a0104, pp. 153\u2013175. North-Holland, Amsterdam (1982)"},{"key":"2_CR9","unstructured":"Platek, R.: Kreisel, Generalized Recursion Theory, Stanford and Me. In: Odifreddi, P. (ed.) Kreiseliana, About and Around Georg Kreisel (1996)"}],"container-title":["Lecture Notes in Computer Science","Computer Science Logic"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-04027-6_2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,3,9]],"date-time":"2019-03-09T14:30:40Z","timestamp":1552141840000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-04027-6_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009]]},"ISBN":["9783642040269","9783642040276"],"references-count":9,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-04027-6_2","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2009]]}}}