{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T22:38:13Z","timestamp":1725489493275},"publisher-location":"Berlin, Heidelberg","reference-count":11,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540427520"},{"type":"electronic","value":"9783540455042"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2001]]},"DOI":"10.1007\/3-540-45504-3_10","type":"book-chapter","created":{"date-parts":[[2007,8,13]],"date-time":"2007-08-13T18:56:02Z","timestamp":1187031362000},"page":"153-169","source":"Crossref","is-referenced-by-count":2,"title":["Interpolation for Natural Deduction with Generalized Eliminations"],"prefix":"10.1007","author":[{"given":"Ralph","family":"Matthes","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2001,10,2]]},"reference":[{"key":"10_CR1","doi-asserted-by":"publisher","first-page":"291","DOI":"10.1007\/BF01270628","volume":"33","author":"\u010c. D. \u010cubri\u0107","year":"1994","unstructured":"[\u010cub94] Djordje \u010cubri\u0107. Interpolation property for bicartesian closed categories. Archive for Mathematical Logic, 33:291\u2013319, 1994.","journal-title":"Archive for Mathematical Logic"},{"key":"10_CR2","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"45","DOI":"10.1007\/3-540-48685-2_4","volume-title":"Rewriting Techniques and Applications","author":"d. P. Groote de","year":"1999","unstructured":"[dG99] Philippe de Groote. On the strong normalisation of natural deduction with permutation-conversions. In Paliath Narendran and Micha\u0451l Rusinowitch, editors, Rewriting Techniques and Applications, 10th International Conference (RTA\u2019 99), Trento, Italy, July 2-4, 1999, Proceedings, volume 1631 of Lecture Notes in Computer Science, pages 45\u201359. Springer Verlag, 1999."},{"key":"10_CR3","unstructured":"[How80] W. A. Howard. The formulae-as-types notion of construction. In J. P. Seldin and J. R. Hindley, editors, To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, pages 479\u2013490. Academic Press, 1980."},{"key":"10_CR4","unstructured":"[JM99] Felix Joachimski and Ralph Matthes. Short proofs of normalization for the simply-typed lambda-calculus, permutative conversions and G\u00f6del\u2019s T. Archive for Mathematical Logic, 1999. Accepted for publication."},{"key":"10_CR5","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"141","DOI":"10.1007\/10721975_10","volume-title":"Rewriting Techniques and Applications","author":"J. F. Joachimski","year":"2000","unstructured":"[JM00] Felix Joachimski and Ralph Matthes. Standardization and confluence for a lambda calculus with generalized applications. In Leo Bachmair, editor, Rewriting Techniques and Applications, Proceedings of the 11th International Conference RTA 2000, Norwich, UK, volume 1833 of Lecture Notes in Computer Science, pages 141\u2013155. Springer Verlag, 2000."},{"key":"10_CR6","unstructured":"[Lei90] Daniel Leivant. Contracting proofs to programs. In Piergiorgio Odifreddi, editor, Logic and Computer Science, volume 31 of APIC Studies in Data Processing, pages 279\u2013327. Academic Press, 1990."},{"key":"10_CR7","unstructured":"[Mat00] Ralph Matthes. Characterizing strongly normalizing terms for a lambda calculus with generalized applications via intersection types. In Jos\u00e1 D. P. Rolim, Andrei Z. Broder, Andrea Corradini, Roberto Gorrieri, Reiko Heckel, Juraj Hromkovic, Ugo Vaccaro, and Joe B. Wells, editors, ICALP Workshops 2000, Proceedings of the Satellite Workshops of the 27th International Colloquium on Automata, Languages, and Programming, Geneva, Switzerland, volume 8 of Proceedings in Informatics, pages 339\u2013353. Carleton Scientific, 2000."},{"key":"10_CR8","doi-asserted-by":"crossref","unstructured":"[Mat01] Ralph Matthes. Tarski\u2019s fixed-point theorem and lambda calculi with monotone inductive types. To appear in Synthese, 2001.","DOI":"10.1023\/A:1020831825964"},{"issue":"1","key":"10_CR9","doi-asserted-by":"publisher","first-page":"33","DOI":"10.2307\/2275175","volume":"57","author":"P. A. Pitts","year":"1992","unstructured":"[Pit92] Andrew Pitts. On an interpretation of second order quantification in first order intuitionistic propositional logic. The Journal of Symbolic Logic, 57(1):33\u201352, 1992.","journal-title":"The Journal of Symbolic Logic"},{"key":"10_CR10","unstructured":"[Pra65] Dag Prawitz. Natural Deduction. A Proof-Theoretical Study. Almquist and Wiksell, 1965."},{"key":"10_CR11","unstructured":"[vP98] Jan von Plato. Natural deduction with general elimination rules. Submitted, 1998."}],"container-title":["Lecture Notes in Computer Science","Proof Theory in Computer Science"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45504-3_10","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,1]],"date-time":"2019-05-01T20:53:18Z","timestamp":1556743998000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45504-3_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001]]},"ISBN":["9783540427520","9783540455042"],"references-count":11,"URL":"https:\/\/doi.org\/10.1007\/3-540-45504-3_10","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2001]]}}}