{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T13:21:06Z","timestamp":1725456066558},"publisher-location":"Berlin\/Heidelberg","reference-count":16,"publisher":"Springer-Verlag","isbn-type":[{"type":"print","value":"354055789X"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/bfb0023777","type":"book-chapter","created":{"date-parts":[[2005,11,19]],"date-time":"2005-11-19T05:11:10Z","timestamp":1132377070000},"page":"316-325","source":"Crossref","is-referenced-by-count":0,"title":["A cut-elimination procedure designed for evaluating proofs as programs"],"prefix":"10.1007","author":[{"given":"Ulf R.","family":"Schmerl","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"24_CR1","doi-asserted-by":"crossref","first-page":"225","DOI":"10.1016\/0304-3975(88)90125-9","volume":"61","author":"M. Alexi","year":"1988","unstructured":"Alexi, M., Extraction and verification of programs by analysis of formal proofs, TCS 61 (1988) 225\u2013258","journal-title":"TCS"},{"key":"24_CR2","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-52756-2","volume-title":"Transfinite Zahlen","author":"H. Bachmann","year":"1955","unstructured":"Bachmann, H., Transfinite Zahlen, Springer Verlag, Berlin 1955"},{"key":"24_CR3","unstructured":"Bates, J.L., A logic for correct program development, Cornell Univ. 1979"},{"key":"24_CR4","unstructured":"Bates, J.L. a. Constable, R.L., Definition of Micro-PRL, Tech. Rp. 82-492, Cornell Univ. 1981"},{"issue":"1","key":"24_CR5","doi-asserted-by":"crossref","first-page":"113","DOI":"10.1145\/2363.2528","volume":"7","author":"J.L. Bates","year":"1985","unstructured":"Bates, J.L. a. Constable, R.L., Proofs as programs, ACM Trans. on Progr. Lang. a. Syst. 7,1 (1985) 113\u2013136","journal-title":"ACM Trans. on Progr. Lang. a. Syst."},{"key":"24_CR6","unstructured":"Bornschein, C., Implementierung eines Verfahrens zur Herleitungstransformation, Diplomarbeit, Technische Universit\u00e4t M\u00fcnchen 1989"},{"issue":"3","key":"24_CR7","doi-asserted-by":"crossref","first-page":"105","DOI":"10.1016\/0020-0190(83)90060-1","volume":"16","author":"R.L. Constable","year":"1983","unstructured":"Constable, R.L., Proofs as Programs, Inf. Process. Lett. 16,3 (1983) 105\u2013112","journal-title":"Inf. Process. Lett."},{"key":"24_CR8","unstructured":"Constable, R.L. a. Bates, J.L., The nearly ultimate PRL, Techn. Rep. 83-551, Cornell Univ. 1983"},{"key":"24_CR9","unstructured":"Gallier, J.H., Logic for Computer Science, New York 1986"},{"key":"24_CR10","doi-asserted-by":"crossref","first-page":"176","DOI":"10.1007\/BF01201353","volume":"39","author":"G. Gentzen","year":"1935","unstructured":"Gentzen, G., Untersuchungen \u00fcber das logische Schlie\u00dfen, Math. Zeitschrift 39 (1935) 176\u2013210, 405\u2013431","journal-title":"Math. Zeitschrift"},{"key":"24_CR11","unstructured":"Hayashi, S., PX: A System extracting Programs from Proofs"},{"issue":"1","key":"24_CR12","first-page":"92","volume":"2","author":"Z. Manna","year":"1980","unstructured":"Manna, Z. a. Waldinger, R., A deductive approach to program synthesis, ACM Trans. on Progr. Lang. a. Syst. 2,1 (1980) 92\u2013121","journal-title":"ACM Trans. on Progr. Lang. a. Syst."},{"key":"24_CR13","unstructured":"Martin-L\u00f6f, P., Constructive mathematics and computer programming, 6th. Intern. Congr. Logic, Method. a. Philos. of Science, Hannover 1979"},{"key":"24_CR14","unstructured":"Regensburger, F., Implementierung eines Schnitteliminationsverfahrens, Diplomarbeit, Technische Universit\u00e4t M\u00fcnchen 1989"},{"key":"24_CR15","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-66473-1","volume-title":"Proof theory","author":"K. Sch\u00fctte","year":"1977","unstructured":"Sch\u00fctte, K., Proof theory, Springer Verlag, Berlin 1977"},{"key":"24_CR16","unstructured":"Schwichtenberg, H., LCF with realizing terms: a framework for the development and verification of programs, 1988"}],"container-title":["Lecture Notes in Computer Science","Computer Science Logic"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0023777.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,12,9]],"date-time":"2020-12-09T16:50:35Z","timestamp":1607532635000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0023777"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["354055789X"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/bfb0023777","relation":{},"subject":[]}}