{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,6]],"date-time":"2026-10-06T14:24:46Z","timestamp":1791296686765,"version":"4.1.0"},"publisher-location":"Berlin, Heidelberg","reference-count":39,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783662496299","type":"print"},{"value":"9783662496305","type":"electronic"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"content-version":"tdm","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":[[2016]]},"DOI":"10.1007\/978-3-662-49630-5_3","type":"book-chapter","created":{"date-parts":[[2016,3,21]],"date-time":"2016-03-21T09:04:32Z","timestamp":1458551072000},"page":"36-54","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":18,"title":["Dependent Types and Fibred Computational Effects"],"prefix":"10.1007","author":[{"given":"Danel","family":"Ahman","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Neil","family":"Ghani","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Gordon D.","family":"Plotkin","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"key":"3_CR1","series-title":"London Mathematical Society Lecture Note Series","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511600579","volume-title":"Locally Presentable and Accessible Categories","author":"J Adamek","year":"1994","unstructured":"Adamek, J., Rosicky, J.: Locally Presentable and Accessible Categories. London Mathematical Society Lecture Note Series. Cambridge University Press, Cambridge (1994)"},{"key":"3_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-3-642-03741-2_2","volume-title":"Algebra and Coalgebra in Computer Science","author":"R Atkey","year":"2009","unstructured":"Atkey, R.: Algebras for parameterised monads. In: Kurz, A., Lenisa, M., Tarlecki, A. (eds.) CALCO 2009. LNCS, vol. 5728, pp. 3\u201317. Springer, Heidelberg (2009)"},{"key":"3_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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. Springer, Heidelberg (1995)"},{"key":"3_CR4","series-title":"Categories and Structures","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511525858","volume-title":"Handbook of Categorical Algebra","author":"F Borceux","year":"1994","unstructured":"Borceux, F.: Handbook of Categorical Algebra. Categories and Structures, vol. 2. Cambridge University Press, Cambridge (1994)"},{"key":"3_CR5","doi-asserted-by":"crossref","unstructured":"Brady, E.: Programming and reasoning with algebraic effects and dependent types. In: Morrisett, G., Uustalu, T. (eds.) Proceedings of 18th International Conference on Functional Programming, ICFP 2013, pp. 133\u2013144. ACM (2013)","DOI":"10.1145\/2500365.2500581"},{"key":"3_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"18","DOI":"10.1007\/978-3-319-14675-1_2","volume-title":"Trends in Functional Programming","author":"E Brady","year":"2015","unstructured":"Brady, E.: Resource-dependent algebraic effects. In: Hage, J., McCarthy, J. (eds.) TFP 2014. LNCS, vol. 8843, pp. 18\u201333. Springer, Heidelberg (2015)"},{"key":"3_CR7","doi-asserted-by":"crossref","unstructured":"Casinghino, C., Sj\u00f6bergberg, V., Weirich, S.: Combining proofs and programs in a dependently typed language. In: Sewell, P. (ed.) Proceedings of 41st Annual Symposium on Principles of Programming Languages, POPL 2014, pp. 33\u201345. ACM (2014)","DOI":"10.1145\/2535838.2535883"},{"key":"3_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"91","DOI":"10.1007\/978-3-642-21691-6_10","volume-title":"Typed Lambda Calculi and Applications","author":"P Clairambault","year":"2011","unstructured":"Clairambault, P., Dybjer, P.: The biequivalence of locally cartesian closed categories and martin-l\u00f6f type theories. In: Ong, L. (ed.) Typed Lambda Calculi and Applications. LNCS, vol. 6690, pp. 91\u2013106. Springer, Heidelberg (2011)"},{"issue":"3","key":"3_CR9","doi-asserted-by":"publisher","first-page":"615","DOI":"10.1093\/logcom\/exs025","volume":"24","author":"J Egger","year":"2014","unstructured":"Egger, J., M\u00f8gelberg, R.E., Simpson, A.: The enriched effect calculus: syntax and semantics. J. Log. Comput. 24(3), 615\u2013654 (2014)","journal-title":"J. Log. Comput."},{"issue":"3:6","key":"3_CR10","doi-asserted-by":"publisher","first-page":"1","DOI":"10.2168\/LMCS-9(3:6)2013","volume":"9","author":"N Ghani","year":"2013","unstructured":"Ghani, N., Johann, P., Fumex, C.: Indexed induction and coinduction, fibrationally. Logical Methods Comput. Sci. 9(3:6), 1\u201331 (2013). doi: 10.2168\/LMCS-9(3:6)2013","journal-title":"Logical Methods Comput. Sci."},{"key":"3_CR11","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511542725","volume-title":"Continuous Lattices and Domains","author":"G Gierz","year":"2003","unstructured":"Gierz, G., Hofmann, K.H., Keimel, K., Lawson, J.D., Mislove, M., Scott, D.S.: Continuous Lattices and Domains. Cambridge University Press, Cambridge (2003)"},{"key":"3_CR12","series-title":"Lecture Notes in Mathematics","doi-asserted-by":"publisher","first-page":"242","DOI":"10.1007\/BFb0081965","volume-title":"Category Theory, Homology Theory and Their Applications III","author":"JW Gray","year":"1969","unstructured":"Gray, J.W.: The categorical comprehension scheme. In: Gray, J.W. (ed.) Category Theory, Homology Theory and Their Applications III. Lecture Notes in Mathematics, vol. 99, pp. 242\u2013312. Springer, Heidelberg (1969)"},{"key":"3_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"317","DOI":"10.1007\/3-540-44622-2_21","volume-title":"CSL 2000","author":"P Hancock","year":"2000","unstructured":"Hancock, P., Setzer, A.: Interactive programs in dependent type theory. In: Clote, P.G., Schwichtenberg, H. (eds.) CSL 2000. LNCS, vol. 1862, pp. 317\u2013331. Springer, Heidelberg (2000)"},{"key":"3_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"427","DOI":"10.1007\/BFb0022273","volume-title":"Computer Science Logic","author":"M Hofmann","year":"1995","unstructured":"Hofmann, M.: On the interpretation of type theory in locally cartesian closed. In: Pacholski, L., Tiuryn, J. (eds.) CSL 1994. LNCS, vol. 933, pp. 427\u2013441. Springer, Heidelberg (1995)"},{"key":"3_CR15","doi-asserted-by":"publisher","first-page":"79","DOI":"10.1017\/CBO9780511526619.004","volume-title":"Semantics and Logics of Computation","author":"M Hofmann","year":"1997","unstructured":"Hofmann, M.: Syntax and semantics of dependent types. In: Pitts, A.M., Dybjer, P. (eds.) Semantics and Logics of Computation, pp. 79\u2013130. Cambridge University Press, Cambridge (1997)"},{"issue":"4","key":"3_CR16","doi-asserted-by":"publisher","first-page":"437","DOI":"10.1017\/S0956796898003050","volume":"8","author":"G Hutton","year":"1998","unstructured":"Hutton, G., Meijer, E.: Monadic parsing in Haskell. J. Funct. Program. 8(4), 437\u2013444 (1998)","journal-title":"J. Funct. Program."},{"issue":"1\u20133","key":"3_CR17","doi-asserted-by":"publisher","first-page":"70","DOI":"10.1016\/j.tcs.2006.03.013","volume":"357","author":"M Hyland","year":"2006","unstructured":"Hyland, M., Plotkin, G., Power, J.: Combining effects: sum and tensor. Theor. Comput. Sci. 357(1\u20133), 70\u201399 (2006)","journal-title":"Theor. Comput. Sci."},{"key":"3_CR18","series-title":"Studies in Logic and the Foundations of Mathematics","volume-title":"Categorical Logic and Type Theory","author":"B Jacobs","year":"1999","unstructured":"Jacobs, B.: Categorical Logic and Type Theory. Studies in Logic and the Foundations of Mathematics, vol. 141. North Holland, Amsterdam (1999)"},{"key":"3_CR19","doi-asserted-by":"crossref","unstructured":"Krishnaswami, N.R., Pradic, P., Benton, N.: Integrating linear and dependent types. In: Walker, D. (ed.) Proceedings of 42nd Annual Symposium on Principles of Programming Languages, POPL 2015, pp. 17\u201330. ACM (2015)","DOI":"10.1145\/2775051.2676969"},{"key":"3_CR20","series-title":"Semantics Structures in Computation","volume-title":"Call-By-Push-Value: A Functional\/Imperative Synthesis","author":"PB Levy","year":"2004","unstructured":"Levy, P.B.: Call-By-Push-Value: A Functional\/Imperative Synthesis. Semantics Structures in Computation, vol. 2. Springer, Heidelberg (2004)"},{"key":"3_CR21","series-title":"Lecture Notes in Mathematics","doi-asserted-by":"publisher","first-page":"75","DOI":"10.1007\/BFb0083082","volume-title":"Seminar on Triples and Categorical Homology Theory","author":"F Linton","year":"1969","unstructured":"Linton, F.: Coequalizers in categories of algebras. In: Eckmann, B. (ed.) Seminar on Triples and Categorical Homology Theory. Lecture Notes in Mathematics, vol. 80, pp. 75\u201390. Springer, Heidelberg (1969)"},{"key":"3_CR22","doi-asserted-by":"crossref","unstructured":"Martin-L\u00f6f, P.: An intuitionisitc theory of types, predicative part. In: Rose, E., Shepherdson, J.C. (eds.) Proceedings of Logic Colloquium 1973, pp. 73\u2013118. North-Holland (1975)","DOI":"10.1016\/S0049-237X(08)71945-1"},{"key":"3_CR23","unstructured":"McBride, C.: Functional pearl: Kleisli arrows of outrageous fortune. J. Funct. Program. (To appear)"},{"key":"3_CR24","doi-asserted-by":"crossref","unstructured":"Moggi, E.: Computational lambda-calculus and monads. In: Parikh, R. (ed.) Proceedings of 4th Annual Symposium on Logic in Computer Science, LICS 1989, pp. 14\u201323. IEEE (1989)","DOI":"10.1109\/LICS.1989.39155"},{"issue":"1","key":"3_CR25","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."},{"issue":"5\u20136","key":"3_CR26","doi-asserted-by":"publisher","first-page":"865","DOI":"10.1017\/S0956796808006953","volume":"18","author":"A Nanevski","year":"2008","unstructured":"Nanevski, A., Morrisett, G., Birkedal, L.: Hoare type theory, polymorphism and separation. J. Funct. Program. 18(5\u20136), 865\u2013911 (2008)","journal-title":"J. Funct. Program."},{"key":"3_CR27","series-title":"Algebraic and Logical Structures","first-page":"39","volume-title":"Handbook of Logic in Computer Science","author":"AM Pitts","year":"2000","unstructured":"Pitts, A.M.: Categorical logic. In: Abramsky, S., Gabbay, D.M., Maibaum, T.S.E. (eds.) Handbook of Logic in Computer Science. Algebraic and Logical Structures, vol. 5, pp. 39\u2013128. Oxford University Press, Oxford (2000). chap. 2"},{"key":"3_CR28","doi-asserted-by":"crossref","unstructured":"Pitts, A.M., Matthiesen, J., Derikx, J.: A dependent type theory with abstractable names. In: Mackie, I., Ayala-Rincon, M. (eds.) Proceedings of 9th Workshop on Logical and Semantic Frameworks, with Applications, LSFA 2014. ENTCS, vol. 312, pp. 19\u201350. Elsevier (2015)","DOI":"10.1016\/j.entcs.2015.04.003"},{"key":"3_CR29","unstructured":"Plotkin, G.: Pisa notes (on domain theory) (1983)"},{"key":"3_CR30","doi-asserted-by":"crossref","unstructured":"Plotkin, G., Power, J.: Semantics for algebraic operations. In: Brookes, S., Mislove, M. (eds.) Proceedings of 17th Conference on the Mathematical Foundations of Programming Semantics, MFPS XVII. ENTCS, vol. 45, pp. 332\u2013345. Elsevier (2001)","DOI":"10.1016\/S1571-0661(04)80970-8"},{"key":"3_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"342","DOI":"10.1007\/3-540-45931-6_24","volume-title":"Foundations of Software Science and Computation Structures","author":"G Plotkin","year":"2002","unstructured":"Plotkin, G., Power, J.: Notions of computation determine monads. In: Nielsen, M., Engberg, U. (eds.) FOSSACS 2002. LNCS, vol. 2303, pp. 342\u2013356. Springer, Heidelberg (2002)"},{"issue":"4:23","key":"3_CR32","doi-asserted-by":"publisher","first-page":"1","DOI":"10.2168\/LMCS-9(4:23)2013","volume":"9","author":"GD Plotkin","year":"2013","unstructured":"Plotkin, G.D., Pretnar, M.: Handling algebraic effects. Logical Methods Comput. Sci. 9(4:23), 1\u201336 (2013). doi: 10.2168\/LMCS-9(4:23)2013","journal-title":"Logical Methods Comput. Sci."},{"key":"3_CR33","doi-asserted-by":"crossref","unstructured":"Power, J.: Countable Lawvere theories and computational effects. In: Seda, A.K., Hurley, T., Schellekens, M., an Airchinnigh, M.M., Strong, G.(eds.) Proceedings of 3rd Irish Conference on the Mathematical Foundations of Computer Science and Information Technology, MFCSIT 2004. ENTCS, vol. 161, pp. 59\u201371. Elsevier (2006)","DOI":"10.1016\/j.entcs.2006.04.025"},{"key":"3_CR34","unstructured":"Pretnar, M.: The Logic and Handling of Algebraic Effects. Ph.D. thesis, School of Informatics, University of Edinburgh (2010)"},{"key":"3_CR35","doi-asserted-by":"crossref","unstructured":"Staton, S.: Instances of computational effects: an algebraic perspective. In: Kupferman, O. (ed.) Proceedings of 28th Annual Symposium on Logic in Computer Science, LICS 2013, pp. 519\u2013519. IEEE, June 2013","DOI":"10.1109\/LICS.2013.58"},{"key":"3_CR36","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-0433-6","volume-title":"Semantics of Type Theory","author":"T Streicher","year":"1991","unstructured":"Streicher, T.: Semantics of Type Theory. Birkh\u00e4user, Boston (1991)"},{"key":"3_CR37","doi-asserted-by":"crossref","unstructured":"Swamy, N., Weinberger, J., Schlesinger, C., Chen, J., Livshits, B.: Verifying higher-order programs with the Dijkstra monad. In: Flanagan, C. (ed.) Proceedings of 34th Conference on Programming Language Design and Implementation, PLDI 2013, pp. 387\u2013398. ACM (2013)","DOI":"10.1145\/2491956.2491978"},{"key":"3_CR38","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"102","DOI":"10.1007\/978-3-662-46678-0_7","volume-title":"Foundations of Software Science and Computation Structures","author":"M V\u00e1k\u00e1r","year":"2015","unstructured":"V\u00e1k\u00e1r, M.: A categorical semantics for linear logical frameworks. In: Pitts, A. (ed.) FOSSACS 2015. LNCS, vol. 9034, pp. 102\u2013116. Springer, Heidelberg (2015)"},{"key":"3_CR39","unstructured":"Warren, M.A.: Homotopy Theoretic Aspects of Constructive Type Theory. Ph.D. thesis, Department of Philosophy, Carnegie Mellon University (2008)"}],"container-title":["Lecture Notes in Computer Science","Foundations of Software Science and Computation Structures"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-662-49630-5_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,1]],"date-time":"2025-06-01T21:30:00Z","timestamp":1748813400000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-662-49630-5_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783662496299","9783662496305"],"references-count":39,"URL":"https:\/\/doi.org\/10.1007\/978-3-662-49630-5_3","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2016]]},"assertion":[{"value":"This content has been made available to all.","name":"free","label":"Free to read"}]}}