{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T10:06:05Z","timestamp":1743069965443,"version":"3.40.3"},"publisher-location":"Cham","reference-count":26,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319661063"},{"type":"electronic","value":"9783319661070"}],"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":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2017]]},"DOI":"10.1007\/978-3-319-66107-0_25","type":"book-chapter","created":{"date-parts":[[2017,8,20]],"date-time":"2017-08-20T14:13:59Z","timestamp":1503238439000},"page":"389-409","source":"Crossref","is-referenced-by-count":2,"title":["Effect Polymorphism in Higher-Order Logic (Proof Pearl)"],"prefix":"10.1007","author":[{"given":"Andreas","family":"Lochbihler","sequence":"first","affiliation":[]}],"member":"297","reference":[{"issue":"2","key":"25_CR1","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1007\/s10817-013-9284-7","volume":"52","author":"C Ballarin","year":"2014","unstructured":"Ballarin, C.: Locales: a module system for mathematical theories. J. Automat. Reason. 52(2), 123\u2013153 (2014)","journal-title":"J. Automat. Reason."},{"key":"25_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1007\/978-3-319-08970-6_7","volume-title":"Interactive Theorem Proving","author":"JC Blanchette","year":"2014","unstructured":"Blanchette, J.C., H\u00f6lzl, J., Lochbihler, A., Panny, L., Popescu, A., Traytel, D.: Truly modular (co)datatypes for Isabelle\/HOL. In: Klein, G., Gamboa, R. (eds.) ITP 2014. LNCS, vol. 8558, pp. 93\u2013110. Springer, Cham (2014). doi:10.1007\/978-3-319-08970-6_7"},{"key":"25_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"134","DOI":"10.1007\/978-3-540-71067-7_14","volume-title":"Theorem Proving in Higher Order Logics","author":"L Bulwahn","year":"2008","unstructured":"Bulwahn, L., Krauss, A., Haftmann, F., Erk\u00f6k, L., Matthews, J.: Imperative functional programming with Isabelle\/HOL. In: Ait Mohamed, O., Mu\u00f1oz, C., Tahar, S. (eds.) TPHOLs 2008. LNCS, vol. 5170, pp. 134\u2013149. Springer, Heidelberg (2008). doi:10.1007\/978-3-540-71067-7_14"},{"key":"25_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"80","DOI":"10.1007\/978-3-662-46669-8_4","volume-title":"Programming Languages and Systems","author":"M Eberl","year":"2015","unstructured":"Eberl, M., H\u00f6lzl, J., Nipkow, T.: A verified compiler for probability density functions. In: Vitek, J. (ed.) ESOP 2015. LNCS, vol. 9032, pp. 80\u2013104. Springer, Heidelberg (2015). doi:10.1007\/978-3-662-46669-8_4"},{"key":"25_CR5","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1017\/S0956796805005721","volume":"16","author":"M Erwig","year":"2006","unstructured":"Erwig, M., Kollmansberger, S.: Functional pearls: probabilistic functional programming in Haskell. J. Funct. Program. 16, 21\u201334 (2006)","journal-title":"J. Funct. Program."},{"key":"25_CR6","doi-asserted-by":"crossref","unstructured":"Gibbons, J., Hinze, R.: Just do it: simple monadic equational reasoning. In: ICFP 2011, pp. 2\u201314. ACM (2011)","DOI":"10.1145\/2034574.2034777"},{"key":"25_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"203","DOI":"10.1007\/978-3-319-22102-1_13","volume-title":"Interactive Theorem Proving","author":"J H\u00f6lzl","year":"2015","unstructured":"H\u00f6lzl, J., Lochbihler, A., Traytel, D.: A formalized hierarchy of probabilistic system types. In: Urban, C., Zhang, X. (eds.) ITP 2015. LNCS, vol. 9236, pp. 203\u2013220. Springer, Cham (2015). doi:10.1007\/978-3-319-22102-1_13"},{"key":"25_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"244","DOI":"10.1007\/978-3-642-03359-9_18","volume-title":"Theorem Proving in Higher Order Logics","author":"PV Homeier","year":"2009","unstructured":"Homeier, P.V.: The HOL-Omega logic. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol. 5674, pp. 244\u2013259. Springer, Heidelberg (2009). doi:10.1007\/978-3-642-03359-9_18"},{"key":"25_CR9","doi-asserted-by":"crossref","unstructured":"Huffman, B.: Formal verification of monad transformers. In: ICFP 2012, pp. 15\u201316. ACM (2012)","DOI":"10.1145\/2398856.2364532"},{"key":"25_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"131","DOI":"10.1007\/978-3-319-03545-1_9","volume-title":"Certified Programs and Proofs","author":"B Huffman","year":"2013","unstructured":"Huffman, B., Kun\u010dar, O.: Lifting and Transfer: a modular design for quotients in Isabelle\/HOL. In: Gonthier, G., Norrish, M. (eds.) CPP 2013. LNCS, vol. 8307, pp. 131\u2013146. Springer, Cham (2013). doi:10.1007\/978-3-319-03545-1_9"},{"key":"25_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"147","DOI":"10.1007\/11541868_10","volume-title":"Theorem Proving in Higher Order Logics","author":"B Huffman","year":"2005","unstructured":"Huffman, B., Matthews, J., White, P.: Axiomatic constructor classes in Isabelle\/HOLCF. In: Hurd, J., Melham, T. (eds.) TPHOLs 2005. LNCS, vol. 3603, pp. 147\u2013162. Springer, Heidelberg (2005). doi:10.1007\/11541868_10"},{"key":"25_CR12","doi-asserted-by":"crossref","unstructured":"Jeuring, J., Jansson, P., Amaral, C.: Testing type class laws. In: Haskell 2012, pp. 49\u201360. ACM (2012)","DOI":"10.1145\/2364506.2364514"},{"key":"25_CR13","doi-asserted-by":"crossref","unstructured":"Kun\u010dar, O.: Correctness of Isabelle\u2019s cyclicity checker: implementability of overloading in proof assistants. In: CPP 2015, pp. 85\u201394. ACM (2015)","DOI":"10.1145\/2676724.2693175"},{"key":"25_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"166","DOI":"10.1007\/978-3-642-32347-8_12","volume-title":"Interactive Theorem Proving","author":"P Lammich","year":"2012","unstructured":"Lammich, P., Tuerk, T.: Applying data refinement for monadic programs to Hopcroft\u2019s algorithm. In: Beringer, L., Felty, A. (eds.) ITP 2012. LNCS, vol. 7406, pp. 166\u2013182. Springer, Heidelberg (2012). doi:10.1007\/978-3-642-32347-8_12"},{"key":"25_CR15","doi-asserted-by":"crossref","unstructured":"Liang, S., Hudak, P., Jones, M.: Monad transformers and modular interpreters. In: POPL 1995, pp. 333\u2013343. ACM (1995)","DOI":"10.1145\/199448.199528"},{"key":"25_CR16","unstructured":"Lobo Vesga, E.: Hacia la formalizaci\u00f3n del razonamiento ecuacional sobre m\u00f3nadas. Technical report, Universidad EAFIT (2013). http:\/\/hdl.handle.net\/10784\/4554"},{"key":"25_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"503","DOI":"10.1007\/978-3-662-49498-1_20","volume-title":"Programming Languages and Systems","author":"A Lochbihler","year":"2016","unstructured":"Lochbihler, A.: Probabilistic functions and cryptographic oracles in higher order logic. In: Thiemann, P. (ed.) ESOP 2016. LNCS, vol. 9632, pp. 503\u2013531. Springer, Heidelberg (2016). doi:10.1007\/978-3-662-49498-1_20"},{"key":"25_CR18","doi-asserted-by":"crossref","unstructured":"Lochbihler, A.: Effect polymorphism in higher-order logic. Archive of Formal Proofs (2017). Formal proof development. http:\/\/isa-afp.org\/entries\/Monomorphic_Monad.shtml","DOI":"10.1007\/978-3-319-66107-0_25"},{"key":"25_CR19","doi-asserted-by":"crossref","unstructured":"Lochbihler, A., Schneider, J.: Equational reasoning with applicative functors. In: Blanchette, J.C., Merz, S. (eds.) ITP 2016. LNCS, vol. 9807, pp. 252\u2013273. Springer, Cham (2016). doi:10.1007\/978-3-319-43144-4_16","DOI":"10.1007\/978-3-319-43144-4_16"},{"key":"25_CR20","doi-asserted-by":"crossref","unstructured":"Mitchell, J.C.: Representation independence and data abstraction. In: POPL 1986, pp. 263\u2013276. ACM (1986)","DOI":"10.1145\/512644.512669"},{"key":"25_CR21","unstructured":"Moggi, E.: An abstract view of programming languages. Technical report ECS-LFCS-90-113, LFCS, School of Informatics, University of Edinburgh (1990)"},{"key":"25_CR22","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-10542-0","volume-title":"Concrete Semantics","author":"T Nipkow","year":"2014","unstructured":"Nipkow, T., Klein, G.: Concrete Semantics. Springer, Cham (2014). doi:10.1007\/978-3-319-10542-0"},{"key":"25_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"385","DOI":"10.1007\/11541868_25","volume-title":"Theorem Proving in Higher Order Logics","author":"T Nipkow","year":"2005","unstructured":"Nipkow, T., Paulson, L.C.: Proof pearl: defining functions over finite sets. In: Hurd, J., Melham, T. (eds.) TPHOLs 2005. LNCS, vol. 3603, pp. 385\u2013396. Springer, Heidelberg (2005). doi:10.1007\/11541868_25"},{"key":"25_CR24","doi-asserted-by":"crossref","unstructured":"Ramsey, N., Pfeffer, A.: Stochastic lambda calculus and monads of probability distributions. In: POPL 2002, pp. 154\u2013165. ACM (2002)","DOI":"10.1145\/565816.503288"},{"key":"25_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"24","DOI":"10.1007\/3-540-59451-5_2","volume-title":"Advanced Functional Programming","author":"P Wadler","year":"1995","unstructured":"Wadler, P.: Monads for functional programming. In: Jeuring, J., Meijer, E. (eds.) AFP 1995. LNCS, vol. 925, pp. 24\u201352. Springer, Heidelberg (1995). doi:10.1007\/3-540-59451-5_2"},{"key":"25_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"307","DOI":"10.1007\/BFb0028402","volume-title":"Theorem Proving in Higher Order Logics","author":"M Wenzel","year":"1997","unstructured":"Wenzel, M.: Type classes and overloading in higher-order logic. In: Gunter, E.L., Felty, A. (eds.) TPHOLs 1997. LNCS, vol. 1275, pp. 307\u2013322. Springer, Heidelberg (1997). doi:10.1007\/BFb0028402"}],"container-title":["Lecture Notes in Computer Science","Interactive Theorem Proving"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-66107-0_25","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,9,29]],"date-time":"2022-09-29T06:07:46Z","timestamp":1664431666000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-66107-0_25"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319661063","9783319661070"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-66107-0_25","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017]]}}}