{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T09:24:46Z","timestamp":1770283486080,"version":"3.49.0"},"publisher-location":"Cham","reference-count":26,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319276823","type":"print"},{"value":"9783319276830","type":"electronic"}],"license":[{"start":{"date-parts":[[2015,12,10]],"date-time":"2015-12-10T00:00:00Z","timestamp":1449705600000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2016]]},"DOI":"10.1007\/978-3-319-27683-0_16","type":"book-chapter","created":{"date-parts":[[2015,12,9]],"date-time":"2015-12-09T21:16:29Z","timestamp":1449695789000},"page":"219-235","source":"Crossref","is-referenced-by-count":9,"title":["Adjoint Logic with a 2-Category of Modes"],"prefix":"10.1007","author":[{"given":"Daniel R.","family":"Licata","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Michael","family":"Shulman","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2015,12,10]]},"reference":[{"issue":"3","key":"16_CR1","doi-asserted-by":"publisher","first-page":"297","DOI":"10.1093\/logcom\/2.3.297","volume":"2","author":"JM Andreoli","year":"1992","unstructured":"Andreoli, J.M.: Logic programming with focusing proofs in linear logic. J. Log. Comput. 2(3), 297\u2013347 (1992)","journal-title":"J. Log. Comput."},{"key":"16_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"121","DOI":"10.1007\/BFb0022251","volume-title":"Computer Science Logic","author":"PN Benton","year":"1995","unstructured":"Benton, P.N.: A mixed linear and non-linear logic: Proofs, terms and models. In: Pacholski, L., Tiuryn, J. (eds.) CSL 1994. LNCS, vol. 933, pp. 121\u2013135. Springer, Heidelberg (1995)"},{"key":"16_CR3","unstructured":"Benton, N., Wadler, P.: Linear logic, monads and the lambda calculus. In: IEEE Symposium on Logic in Computer Science. IEEE Computer Society Press (1996)"},{"key":"16_CR4","unstructured":"Bezem, M., Coquand, T., Huber, S.: A model of type theory in cubical sets. preprint, September 2013"},{"key":"16_CR5","unstructured":"Cavallo, E.: The Mayer-Vietoris sequence in HoTT. In: Talk at Oxford Workshop on Homotopy Type Theory, November 2014"},{"key":"16_CR6","doi-asserted-by":"crossref","unstructured":"Hou, K.B.: Covering spaces in homotopy type theory, talk at TYPES, May 2014","DOI":"10.1007\/978-3-319-21284-5_15"},{"key":"16_CR7","unstructured":"Kapulkin, C., Lumsdaine, P.L., Voevodsky, V.: The simplicial model of univalent foundations (2012). \n                    arXiv:1211.2851"},{"issue":"3","key":"16_CR8","first-page":"41","volume":"19","author":"FW Lawvere","year":"2007","unstructured":"Lawvere, F.W.: Axiomatic cohesion. Theory Appl. Categories 19(3), 41\u201349 (2007)","journal-title":"Theory Appl. Categories"},{"key":"16_CR9","doi-asserted-by":"crossref","unstructured":"Licata, D.R., Brunerie, G.: \n                    \n                      \n                    \n                    $$\\pi _n(S^n)$$\n                   in homotopy type theory. In: Certified Programs and Proofs (2013)","DOI":"10.1007\/978-3-319-03545-1_1"},{"key":"16_CR10","doi-asserted-by":"crossref","unstructured":"Licata, D.R., Brunerie, G.: A cubical approach to synthetic homotopy theory. In: IEEE Symposium on Logic in Computer Science (2015)","DOI":"10.1109\/LICS.2015.19"},{"key":"16_CR11","doi-asserted-by":"crossref","unstructured":"Licata, D.R., Finster, E.: Eilenberg-MacLane spaces in homotopy type theory. In: IEEE Symposium on Logic in Computer Science (2014)","DOI":"10.1145\/2603088.2603153"},{"key":"16_CR12","doi-asserted-by":"crossref","unstructured":"Licata, D.R., Shulman, M.: Calculating the fundamental group of the circle in homotopy type theory. In: IEEE Symposium on Logic in Computer Science (2013)","DOI":"10.1109\/LICS.2013.28"},{"key":"16_CR13","unstructured":"Lumsdaine, P.L.: Higher inductive types: a tour of the menagerie, April 2011. \n                    https:\/\/homotopytypetheory.org\/2011\/04\/24\/higher-inductive-types-a-tour-of-the-menagerie\/"},{"key":"16_CR14","unstructured":"Lumsdaine, P.L., Shulman, M.: Higher inductive types, (in preparation 2015)"},{"key":"16_CR15","series-title":"Graduate Texts in Mathematics","volume-title":"Categories for the Working Mathematician","author":"S MacLane","year":"1998","unstructured":"MacLane, S.: Categories for the Working Mathematician. Graduate Texts in Mathematics, vol. 5, 2nd edn. Springer, New York (1998)","edition":"2"},{"issue":"1","key":"16_CR16","doi-asserted-by":"publisher","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":"16_CR17","unstructured":"Norell, U.: Towards a practical programming language based on dependent type theory. Ph.D. thesis, Chalmers University of Technology (2007)"},{"key":"16_CR18","doi-asserted-by":"publisher","first-page":"511","DOI":"10.1017\/S0960129501003322","volume":"11","author":"F Pfenning","year":"2001","unstructured":"Pfenning, F., Davies, R.: A judgmental reconstruction of modal logic. Math. Struct. Comput. Sci. 11, 511\u2013540 (2001)","journal-title":"Math. Struct. Comput. Sci."},{"key":"16_CR19","unstructured":"Reed, J.: A judgemental deconstruction of modal logic (2009). Accessed \n                    www.cs.cmu.edu\/jcreed\/papers\/jdml.pdf"},{"key":"16_CR20","unstructured":"Schreiber, U.: Differential cohomology in a cohesive \n                    \n                      \n                    \n                    $$\\infty $$\n                  -topos (2013). \n                    arXiv:1310.7930"},{"key":"16_CR21","unstructured":"Schreiber, U., Shulman, M.: Quantum gauge field theory in cohesive homotopy type theory. In: Workshop on Quantum Physics and Logic (2012)"},{"key":"16_CR22","unstructured":"Shulman, M.: Homotopy type theory VI: higher inductive types, April 2011. \n                    https:\/\/golem.ph.utexas.edu\/category\/2011\/04\/homotopy_type_theory_vi.html"},{"key":"16_CR23","unstructured":"Shulman, M.: Brouwer\u2019s fixed-point theorem in real-cohesive homotopy type theory (2015). \n                    arXiv:1509.07584"},{"issue":"5","key":"16_CR24","doi-asserted-by":"crossref","first-page":"1203","DOI":"10.1017\/S0960129514000565","volume":"25","author":"MICHAEL SHULMAN","year":"2014","unstructured":"Shulman, M.: Univalence for inverse diagrams and homotopy canonicity. Math. Struct. Comput. Sci. 25, 1203\u20131277 (2015) \n                    arXiv:1203.3253","journal-title":"Mathematical Structures in Computer Science"},{"key":"16_CR25","unstructured":"Univalent Foundations Program: Homotopy Type Theory: Univalent Foundations of Mathematics (2013). Accessed \n                    homotopytypetheory.org\/book"},{"key":"16_CR26","unstructured":"Voevodsky, V.: A very short note on homotopy \n                    \n                      \n                    \n                    $$\\lambda $$\n                  -calculus, September 2006. \n                    https:\/\/www.math.ias.edu\/vladimir\/files\/2006_09_Hlambda.pdf"}],"container-title":["Lecture Notes in Computer Science","Logical Foundations of Computer Science"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-27683-0_16","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,31]],"date-time":"2019-05-31T21:32:26Z","timestamp":1559338346000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-27683-0_16"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015,12,10]]},"ISBN":["9783319276823","9783319276830"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-27683-0_16","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015,12,10]]}}}