{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,7]],"date-time":"2024-09-07T19:49:15Z","timestamp":1725738555214},"publisher-location":"Berlin, Heidelberg","reference-count":15,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642392115"},{"type":"electronic","value":"9783642392122"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-39212-2_36","type":"book-chapter","created":{"date-parts":[[2013,7,2]],"date-time":"2013-07-02T13:09:19Z","timestamp":1372770559000},"page":"398-409","source":"Crossref","is-referenced-by-count":5,"title":["Proof Systems for Retracts in Simply Typed Lambda Calculus"],"prefix":"10.1007","author":[{"given":"Colin","family":"Stirling","sequence":"first","affiliation":[]}],"member":"297","reference":[{"doi-asserted-by":"crossref","unstructured":"Barendregt, H.: Lambda calculi with types. In: Abramsky, S., Gabbay, D., Maibaum, T. (eds.) Handbook of Logic in Computer Science, vol.\u00a02, pp. 118\u2013309. Oxford University Press (1992)","key":"36_CR1","DOI":"10.1093\/oso\/9780198537618.003.0002"},{"doi-asserted-by":"crossref","unstructured":"Bruce, K., Longo, G.: Provable isomorphisms and domain equations in models of typed languages. In: Proc. 17th Symposium on Theory of Computing, pp. 263\u2013272. ACM (1985)","key":"36_CR2","DOI":"10.1145\/22145.22175"},{"unstructured":"de \u2019Liguoro, U., Piperno, A., Statman, R.: Retracts in simply typed \u03bb\u03b2\u03b7-calculus. In: Procs. LICS 1992, pp. 461\u2013469 (1992)","key":"36_CR3"},{"issue":"1","key":"36_CR4","doi-asserted-by":"publisher","first-page":"51","DOI":"10.1093\/jigpal\/11.1.51","volume":"11","author":"R. Loader","year":"2003","unstructured":"Loader, R.: Higher-order \u03b2-matching is undecidable. Logic Journal of the IGPL\u00a011(1), 51\u201368 (2003)","journal-title":"Logic Journal of the IGPL"},{"unstructured":"Ong, C.-H.L.: On model-checking trees generated by higher-order recursion schemes. In: Procs. LICS 2006, pp. 81\u201390 (2006)","key":"36_CR5"},{"doi-asserted-by":"crossref","unstructured":"Ong, C.-H.L., Tzevelekos, N.: Functional Reachability. In: Procs. LICS 2009, pp. 286\u2013295 (2009)","key":"36_CR6","DOI":"10.1109\/LICS.2009.48"},{"issue":"3","key":"36_CR7","doi-asserted-by":"publisher","first-page":"361","DOI":"10.1017\/S0960129500003108","volume":"10","author":"V. Padovani","year":"2000","unstructured":"Padovani, V.: Decidability of fourth-order matching. Mathematical Structures in Computer Science\u00a010(3), 361\u2013372 (2000)","journal-title":"Mathematical Structures in Computer Science"},{"key":"36_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"376","DOI":"10.1007\/3-540-45413-6_29","volume-title":"Typed Lambda Calculi and Applications","author":"V. Padovani","year":"2001","unstructured":"Padovani, V.: Retracts in simple types. In: Abramsky, S. (ed.) TLCA 2001. LNCS, vol.\u00a02044, pp. 376\u2013384. Springer, Heidelberg (2001)"},{"unstructured":"Regnier, L., Urzyczyn, P.: Retractions of types with many atoms, pp. 1\u201316 (2005), http:\/\/arxiv.org\/abs\/cs\/0212005","key":"36_CR9"},{"key":"36_CR10","doi-asserted-by":"publisher","first-page":"753","DOI":"10.1017\/S096012950800683X","volume":"18","author":"A. Schubert","year":"2008","unstructured":"Schubert, A.: On the building of affine retractions. Math. Struct. in Comp. Science\u00a018, 753\u2013793 (2008)","journal-title":"Math. Struct. in Comp. Science"},{"doi-asserted-by":"crossref","unstructured":"Stirling, C.: Higher-order matching, games and automata. In: Procs. LICS 2007, pp. 326\u2013335 (2007)","key":"36_CR11","DOI":"10.1109\/LICS.2007.23"},{"key":"36_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"92","DOI":"10.1007\/978-3-642-00596-1_8","volume-title":"Foundations of Software Science and Computational Structures","author":"C. Stirling","year":"2009","unstructured":"Stirling, C.: Dependency tree automata. In: de Alfaro, L. (ed.) FOSSACS 2009. LNCS, vol.\u00a05504, pp. 92\u2013106. Springer, Heidelberg (2009)"},{"issue":"3:2","key":"36_CR13","first-page":"1","volume":"5","author":"C. Stirling","year":"2009","unstructured":"Stirling, C.: Decidability of higher-order matching. Logical Methods in Computer Science\u00a05(3:2), 1\u201352 (2009)","journal-title":"Logical Methods in Computer Science"},{"unstructured":"Stirling, C.: An introduction to decidability of higher-order matching (2012) (Submitted for Publication), Availble at author\u2019s website","key":"36_CR14"},{"unstructured":"Vorobyov, S.: The \u201chardest\u201d natural decidable theory. In: Procs. LICS 1997, pp. 294\u2013305 (1997)","key":"36_CR15"}],"container-title":["Lecture Notes in Computer Science","Automata, Languages, and Programming"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-39212-2_36","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,5,13]],"date-time":"2024-05-13T16:48:03Z","timestamp":1715618883000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-39212-2_36"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642392115","9783642392122"],"references-count":15,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-39212-2_36","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2013]]}}}