{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,9]],"date-time":"2024-09-09T22:35:47Z","timestamp":1725921347510},"publisher-location":"Cham","reference-count":22,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319712369"},{"type":"electronic","value":"9783319712376"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2017]]},"DOI":"10.1007\/978-3-319-71237-6_20","type":"book-chapter","created":{"date-parts":[[2017,11,18]],"date-time":"2017-11-18T01:13:02Z","timestamp":1510967582000},"page":"406-425","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Partiality and Container Monads"],"prefix":"10.1007","author":[{"given":"Tarmo","family":"Uustalu","sequence":"first","affiliation":[]},{"given":"Niccol\u00f2","family":"Veltri","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2017,11,19]]},"reference":[{"issue":"1","key":"20_CR1","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1016\/j.tcs.2005.06.002","volume":"342","author":"M Abbott","year":"2005","unstructured":"Abbott, M., Altenkirch, T., Ghani, N.: Containers: constructing strictly positive types. Theor. Comput. Sci. 342(1), 3\u201327 (2005)","journal-title":"Theor. Comput. Sci."},{"key":"20_CR2","doi-asserted-by":"crossref","unstructured":"Ahman, D., Chapman, J., Uustalu, T.: When is a container a comonad? Log. Methods Comput. Sci. 10(3), article 14 (2014)","DOI":"10.2168\/LMCS-10(3:14)2014"},{"key":"20_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"534","DOI":"10.1007\/978-3-662-54458-7_31","volume-title":"Foundations of Software Science and Computation Structures","author":"T Altenkirch","year":"2017","unstructured":"Altenkirch, T., Danielsson, N.A., Kraus, N.: Partiality, revisited. The partiality monad as a quotient inductive-inductive type. In: Esparza, J., Murawski, A.S. (eds.) FoSSaCS 2017. LNCS, vol. 10203, pp. 534\u2013549. Springer, Heidelberg (2017). \nhttps:\/\/doi.org\/10.1007\/978-3-662-54458-7_31"},{"key":"20_CR4","unstructured":"Altenkirch, T., Pinyo, G.: Monadic containers and universes (abstract). In: Kaposi, A. (ed.) Abstracts of 23rd International Conference on Types for Proofs and Programs, TYPES 2017, pp. 20\u201321. E\u00f6tv\u00f6s L\u00f3rand University, Budapest (2017)"},{"issue":"1","key":"20_CR5","doi-asserted-by":"crossref","first-page":"38","DOI":"10.1017\/S0960129514000115","volume":"26","author":"A Bove","year":"2016","unstructured":"Bove, A., Krauss, A., Sozeau, M.: Partiality and recursion in interactive theorem provers\u2013an overview. Math. Struct. Comput. Sci. 26(1), 38\u201388 (2016)","journal-title":"Math. Struct. Comput. Sci."},{"issue":"1\u20132","key":"20_CR6","doi-asserted-by":"crossref","first-page":"31","DOI":"10.1016\/S0304-3975(01)00243-2","volume":"294","author":"A Bucalo","year":"2003","unstructured":"Bucalo, A., F\u00fchrmann, C., Simpson, A.: An equational notion of lifting monad. Theor. Comput. Sci. 294(1\u20132), 31\u201360 (2003)","journal-title":"Theor. Comput. Sci."},{"key":"20_CR7","doi-asserted-by":"crossref","unstructured":"Capretta, V.: General recursion via coinductive types. Log. Methods Comput. Sci. 1(2), Article 1 (2005)","DOI":"10.2168\/LMCS-1(2:1)2005"},{"key":"20_CR8","doi-asserted-by":"crossref","unstructured":"Chapman, J., Uustalu, T., Veltri, N.: Quotienting the delay monad by weak bisimilarity. Math. Struct. Comput. Sci. (to appear)","DOI":"10.1007\/978-3-319-25150-9_8"},{"issue":"1\u20132","key":"20_CR9","doi-asserted-by":"crossref","first-page":"223","DOI":"10.1016\/S0304-3975(00)00382-0","volume":"270","author":"JRB Cockett","year":"2002","unstructured":"Cockett, J.R.B., Lack, S.: Restriction categories I: categories of partial maps. Theor. Comput. Sci. 270(1\u20132), 223\u2013259 (2002)","journal-title":"Theor. Comput. Sci."},{"issue":"1\u20132","key":"20_CR10","doi-asserted-by":"crossref","first-page":"61","DOI":"10.1016\/S0304-3975(01)00245-6","volume":"294","author":"JRB Cockett","year":"2003","unstructured":"Cockett, J.R.B., Lack, S.: Restriction categories II: partial map classification. Theor. Comput. Sci 294(1\u20132), 61\u2013102 (2003)","journal-title":"Theor. Comput. Sci"},{"issue":"4","key":"20_CR11","doi-asserted-by":"crossref","first-page":"775","DOI":"10.1017\/S0960129507006056","volume":"17","author":"JRB Cockett","year":"2007","unstructured":"Cockett, J.R.B., Lack, S.: Restriction categories III: colimits, partial limits, and extensivity. Math. Struct. Comput. Sci. 17(4), 775\u2013817 (2007)","journal-title":"Math. Struct. Comput. Sci."},{"key":"20_CR12","doi-asserted-by":"crossref","unstructured":"Coquand, T., Mannaa, B., Ruch, F.: Stack semantics of type theory. In: Proceedings of 32th Annual ACM\/IEEE Symposium on Logic in Computer Science, LICS 2017 (2017)","DOI":"10.1109\/LICS.2017.8005130"},{"key":"20_CR13","first-page":"21","volume":"87","author":"MH Escard\u00f3","year":"2004","unstructured":"Escard\u00f3, M.H.: Synthetic topology of data types and classical spaces. Electron. Notes Theor. Comput. Sci. 87, 21\u2013156 (2004)","journal-title":"Electron. Notes Theor. Comput. Sci."},{"key":"20_CR14","unstructured":"Escard\u00f3, M.H., Knapp, C.M.: Partial elements and recursion via dominances in univalent type theory. In: Goranko, V., Dam, M. (eds.) Proceedings of 26th EACSL Annual Conference on Computer Science Logic, CSL 2017, Leibniz International Proceedings in Informatics, vol. 82, article 21. Dagstuhl Publishing, Saarbr\u00fccken\/Wadern (2017)"},{"key":"20_CR15","volume-title":"Topos Theory. London Mathematical Society Monographs","author":"PT Johnstone","year":"1977","unstructured":"Johnstone, P.T.: Topos Theory. London Mathematical Society Monographs, vol. 10. Cambridge University Press, Cambridge (1977)"},{"issue":"1","key":"20_CR16","doi-asserted-by":"crossref","first-page":"55","DOI":"10.1016\/0890-5401(91)90052-4","volume":"93","author":"E Moggi","year":"1991","unstructured":"Moggi, E.: Notions of computation and monads. Inf. Comput. 93(1), 55\u201392 (1991)","journal-title":"Inf. Comput."},{"key":"20_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"230","DOI":"10.1007\/978-3-642-04652-0_5","volume-title":"Advanced Functional Programming","author":"U Norell","year":"2009","unstructured":"Norell, U.: Dependently typed programming in Agda. In: Koopman, P., Plasmeijer, R., Swierstra, D. (eds.) AFP 2008. LNCS, vol. 5832, pp. 230\u2013266. Springer, Heidelberg (2009). \nhttps:\/\/doi.org\/10.1007\/978-3-642-04652-0_5"},{"issue":"2","key":"20_CR18","doi-asserted-by":"crossref","first-page":"95","DOI":"10.1016\/0890-5401(88)90034-X","volume":"79","author":"E Robinson","year":"1988","unstructured":"Robinson, E., Rosolini, G.: Categories of partial maps. Inf. Comput. 79(2), 95\u2013130 (1988)","journal-title":"Inf. Comput."},{"key":"20_CR19","unstructured":"Rosolini, G.: Continuity and Effectiveness in Topoi. DPhil thesis, University of Oxford (1986)"},{"key":"20_CR20","unstructured":"Univalent Foundations Program, The: Homotopy Type theory: Univalent Foundations of Mathematics. Institute for Advanced Study, Princeton, NJ (2013). \nhttp:\/\/homotopytypetheory.org\/book"},{"key":"20_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"91","DOI":"10.1007\/978-3-319-68953-1_8","volume-title":"Topics in Theoretical Computer Science","author":"T Uustalu","year":"2017","unstructured":"Uustalu, T.: Container combinatorics: monads and lax monoidal functors. In: Mousavi, M.R., Sgall, J. (eds.) TTCS 2017. LNCS, vol. 10608, pp. 91\u2013105. Springer, Heidelberg (2017). \nhttps:\/\/doi.org\/10.1007\/978-3-319-68953-1_8"},{"key":"20_CR22","doi-asserted-by":"publisher","first-page":"32","DOI":"10.1007\/978-3-319-67729-3_3","volume-title":"Theoretical Aspects of Computing","author":"T Uustalu","year":"2017","unstructured":"Uustalu, T., Veltri, N.: The delay monad and restriction categories. In: Hung, D.V., Kapur, D. (eds.) ICTAC 2017. LNCS, vol. 10580, pp. 32\u201350. Springer, Heidelberg (2017). \nhttps:\/\/doi.org\/10.1007\/978-3-319-67729-3_3"}],"container-title":["Lecture Notes in Computer Science","Programming Languages and Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-71237-6_20","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2017,11,18]],"date-time":"2017-11-18T01:20:38Z","timestamp":1510968038000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-71237-6_20"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319712369","9783319712376"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-71237-6_20","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017]]}}}