{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,1,10]],"date-time":"2023-01-10T00:09:23Z","timestamp":1673309363922},"reference-count":9,"publisher":"Springer Science and Business Media LLC","issue":"5","license":[{"start":{"date-parts":[[2021,1,21]],"date-time":"2021-01-21T00:00:00Z","timestamp":1611187200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2021,1,21]],"date-time":"2021-01-21T00:00:00Z","timestamp":1611187200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Stud Logica"],"published-print":{"date-parts":[[2021,10]]},"DOI":"10.1007\/s11225-020-09931-0","type":"journal-article","created":{"date-parts":[[2021,1,21]],"date-time":"2021-01-21T11:03:57Z","timestamp":1611227037000},"page":"917-936","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Confluence Proofs of Lambda-Mu-Calculi by Z Theorem"],"prefix":"10.1007","volume":"109","author":[{"given":"Yuki","family":"Honda","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Koji","family":"Nakazawa","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ken-etsu","family":"Fujita","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2021,1,21]]},"reference":[{"key":"9931_CR1","doi-asserted-by":"publisher","first-page":"52","DOI":"10.1016\/S1571-0661(04)80878-8","volume":"42","author":"K Baba","year":"2001","unstructured":"Baba, K., S. Hirokawa, and K. Fujita, Parallel reduction in type free $$\\lambda \\mu $$-calculus, Electronic Notes in Theoretical Computer Science 42:52\u201366, 2001.","journal-title":"Electronic Notes in Theoretical Computer Science"},{"key":"9931_CR2","unstructured":"Dehornoy, P., and V. van Oostrom, Z. Proving confluence by monotonic single-step upperbound functions, in Logical Models of Reasoning and Computation (LMRC-08), 2008."},{"key":"9931_CR3","doi-asserted-by":"crossref","unstructured":"Fujita, K., Explicitly typed $$\\lambda \\mu $$-calculus for polymorphism and call-by-value, in Typed Lambda Calculi and Applications, 4th International Conference (TLCA 1999), volume 1581 of Lecture Notes in Computer Science, 1999, pp. 162\u2013176.","DOI":"10.1007\/3-540-48959-2_13"},{"key":"9931_CR4","doi-asserted-by":"publisher","first-page":"433","DOI":"10.1051\/ita:2000102","volume":"34","author":"K Fujita","year":"2000","unstructured":"Fujita, K., Domain-free $$\\lambda \\mu $$-calculus, Theoretical Informatics and Applications 34:433\u2013466, 2000.","journal-title":"Theoretical Informatics and Applications"},{"key":"9931_CR5","doi-asserted-by":"publisher","first-page":"429","DOI":"10.1016\/S0304-3975(01)00380-2","volume":"290","author":"K Nakazawa","year":"2003","unstructured":"Nakazawa,\u00a0K., Confluency and strong normalizability of call-by-value $$\\lambda \\mu $$-calculus, Theoretical Computer Science 290:429\u2013463, 2003.","journal-title":"Theoretical Computer Science"},{"key":"9931_CR6","doi-asserted-by":"publisher","first-page":"1205","DOI":"10.1007\/s11225-016-9673-0","volume":"104","author":"K Nakazawa","year":"2016","unstructured":"Nakazawa,\u00a0K., and K. Fujita, Compositional Z: Confluence proofs for permutative conversion, Studia Logica 104:1205\u20131224, 2016.","journal-title":"Studia Logica"},{"key":"9931_CR7","doi-asserted-by":"crossref","unstructured":"Ong,\u00a0C.-H.L., and C. A. Stewart, A curry-howard foundation for functional computation with control, in 24th Annual ACM Symposium of Principles of Programming Languages (POPL 1997), 1997, pp. 215\u2013227.","DOI":"10.1145\/263699.263722"},{"key":"9931_CR8","doi-asserted-by":"crossref","unstructured":"Parigot, M., $$\\lambda \\mu $$-calculus: an algorithmic interpretation of classical natural deduction, in Proceedings of the International Conference on Logic Programming and Automated Reasoning (LPAR \u201992), volume 624 of Lecture Notes in Computer Science, Springer, 1992, pp. 190\u2013201.","DOI":"10.1007\/BFb0013061"},{"key":"9931_CR9","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/1805950.1805958","volume":"11","author":"A Saurin","year":"2010","unstructured":"Saurin, A., Typing streams in the $$\\Lambda \\mu $$-calculus, ACM Transactions on Computational Logic 11:1\u201334, 2010.","journal-title":"ACM Transactions on Computational Logic"}],"container-title":["Studia Logica"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s11225-020-09931-0.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s11225-020-09931-0\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s11225-020-09931-0.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,9,21]],"date-time":"2021-09-21T16:07:57Z","timestamp":1632240477000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s11225-020-09931-0"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,1,21]]},"references-count":9,"journal-issue":{"issue":"5","published-print":{"date-parts":[[2021,10]]}},"alternative-id":["9931"],"URL":"https:\/\/doi.org\/10.1007\/s11225-020-09931-0","relation":{},"ISSN":["0039-3215","1572-8730"],"issn-type":[{"value":"0039-3215","type":"print"},{"value":"1572-8730","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021,1,21]]},"assertion":[{"value":"11 August 2020","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"21 January 2021","order":2,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}