{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T23:18:13Z","timestamp":1725664693175},"publisher-location":"Berlin, Heidelberg","reference-count":10,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540633853"},{"type":"electronic","value":"9783540698067"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1997]]},"DOI":"10.1007\/3-540-63385-5_50","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T23:26:32Z","timestamp":1330298792000},"page":"278-289","source":"Crossref","is-referenced-by-count":0,"title":["Translating set theoretical proofs into type theoretical programs"],"prefix":"10.1007","author":[{"given":"Anton","family":"Setzer","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,6,8]]},"reference":[{"key":"23_CR1","doi-asserted-by":"crossref","unstructured":"Barwise, J.: Admissible Sets and Structures. An Approach to Definability Theory, Springer, 1975.","DOI":"10.1007\/978-3-662-11035-5"},{"key":"23_CR2","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-68952-9","volume-title":"Foundations of Constructive Mathematics","author":"M. Beeson","year":"1985","unstructured":"Beeson, M.: Foundations of Constructive Mathematics Springer, Berlin, 1985"},{"key":"23_CR3","doi-asserted-by":"crossref","unstructured":"Berger, U. and Schwichtenberg, H.: Program Extraction from Classical Proofs. In: D. Leivant (Ed.): Logic and Computational Complexity, LCC '94, Indianapolis, October 1994, Springer Lecture Notes in Computer Science 960, pp. 77\u201397.","DOI":"10.1007\/3-540-60178-3_80"},{"key":"23_CR4","doi-asserted-by":"crossref","first-page":"277","DOI":"10.1007\/BF01621472","volume":"30","author":"W. Buchholz","year":"1991","unstructured":"Buchholz, W.: Notation systems for infinitary derivations. Arch. Math. Logic (1991) 30:277\u2013296.","journal-title":"Arch. Math. Logic"},{"key":"23_CR5","first-page":"115","volume-title":"Proof Theory","author":"W. Buchholz","year":"1992","unstructured":"Buchholz, W.: A simplified version of local predicativity. In: Aczel, P. et al. (Eds.): Proof Theory. Cambridge University Press, Cambridge, 1992, pp. 115\u2013147."},{"key":"23_CR6","volume-title":"Theories for Admissible Sets: A Unifying Approach to Proof Theory","author":"G. J\u00e4ger","year":"1986","unstructured":"J\u00e4ger, G.: Theories for Admissible Sets: A Unifying Approach to Proof Theory. Bibliopolis, Naples, 1986."},{"key":"23_CR7","first-page":"81","volume-title":"Proof Theory","author":"H. Schwichtenberg","year":"1992","unstructured":"Schwichtenberg, H.: Proofs as programs. In:Aczel, P. et al. (Eds.): Proof Theory. Cambridge University Press, Cambridge, 1992, pp. 81\u2013113."},{"key":"23_CR8","unstructured":"Setzer, A.: Proof theoretical strength of Martin-L\u00f6f Type Theory with W-type and one universe. PhD-thesis, Munich, 1993."},{"key":"23_CR9","unstructured":"Setzer, A.: Extending Martin-L\u00f6f Type Theory by one Mahlo-Universe. Submitted."},{"key":"23_CR10","unstructured":"Setzer, A.: Well-ordering proofs for Martin-L\u00f6f Type Theory with W-type and one universe. Submitted."}],"container-title":["Lecture Notes in Computer Science","Computational Logic and Proof Theory"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-63385-5_50.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T21:18:22Z","timestamp":1605647902000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-63385-5_50"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1997]]},"ISBN":["9783540633853","9783540698067"],"references-count":10,"URL":"https:\/\/doi.org\/10.1007\/3-540-63385-5_50","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1997]]}}}