{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,20]],"date-time":"2025-07-20T03:35:33Z","timestamp":1752982533545,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":21,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783662466681"},{"type":"electronic","value":"9783662466698"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-662-46669-8_4","type":"book-chapter","created":{"date-parts":[[2015,4,1]],"date-time":"2015-04-01T14:37:37Z","timestamp":1427899057000},"page":"80-104","source":"Crossref","is-referenced-by-count":17,"title":["A Verified Compiler for Probability Density Functions"],"prefix":"10.1007","author":[{"given":"Manuel","family":"Eberl","sequence":"first","affiliation":[]},{"given":"Johannes","family":"H\u00f6lzl","sequence":"additional","affiliation":[]},{"given":"Tobias","family":"Nipkow","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"4_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1007\/11783596_6","volume-title":"Mathematics of Program Construction","author":"P. Audebaud","year":"2006","unstructured":"Audebaud, P., Paulin-Mohring, C.: Proofs of randomized algorithms in Coq. In: Uustalu, T. (ed.) MPC 2006. LNCS, vol.\u00a04014, pp. 49\u201368. Springer, Heidelberg (2006), \n                    \n                      http:\/\/dx.doi.org\/10.1007\/11783596_6"},{"key":"4_CR2","unstructured":"Avigad, J., H\u00f6lzl, J., Serafin, L.: A formally verified proof of the Central Limit Theorem. CoRR abs\/1405.7012 (2014)"},{"key":"4_CR3","doi-asserted-by":"crossref","unstructured":"Bertot, Y., Cast\u00e9ran, P.: Interactive Theorem Proving and Program Development. Coq\u2019Art: The Calculus of Inductive Constructions. Springer (2004)","DOI":"10.1007\/978-3-662-07964-5"},{"key":"4_CR4","first-page":"545","volume-title":"Proceedings of the 39th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2012","author":"S. Bhat","year":"2012","unstructured":"Bhat, S., Agarwal, A., Vuduc, R., Gray, A.: A type theory for probability density functions. In: Proceedings of the 39th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2012, pp. 545\u2013556. ACM, New York (2012), \n                    \n                      http:\/\/doi.acm.org\/10.1145\/2103656.2103721"},{"key":"4_CR5","doi-asserted-by":"crossref","unstructured":"Bhat, S., Borgstr\u00f6m, J., Gordon, A.D., Russo, C.: Deriving probability density functions from probabilistic functional programs. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013. LNCS, vol.\u00a07795, pp. 508\u2013522. Springer, Heidelberg (2013), \n                    \n                      http:\/\/dx.doi.org\/10.1007\/978-3-642-36742-7_35","DOI":"10.1007\/978-3-642-36742-7_35"},{"key":"4_CR6","unstructured":"Bhat, S., Borgstr\u00f6m, J., Gordon, A.D., Russo, C.: Deriving probability density functions from probabilistic functional programs (full version, submitted for publication)"},{"key":"4_CR7","doi-asserted-by":"publisher","first-page":"381","DOI":"10.1016\/1385-7258(72)90034-0","volume":"34","author":"N.G. Bruijn de","year":"1972","unstructured":"de Bruijn, N.G.: Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser theorem. Indagationes Mathematicae\u00a034, 381\u2013392 (1972)","journal-title":"Indagationes Mathematicae"},{"key":"4_CR8","unstructured":"Cock, D.: Verifying probabilistic correctness in Isabelle with pGCL. In: Proceedings of the 7th Systems Software Verification, pp. 1\u201310 (November 2012)"},{"key":"4_CR9","unstructured":"Cock, D.: pGCL for Isabelle. Archive of Formal Proofs Formal proof development (July 2014), \n                    \n                      http:\/\/afp.sf.net\/entries\/pGCL.shtml"},{"key":"4_CR10","doi-asserted-by":"crossref","unstructured":"Doberkat, E.E.: Stochastic relations: foundations for Markov transition systems. Studies in Informatics. Chapman & Hall\/CRC (2007)","DOI":"10.1201\/9781584889427"},{"key":"4_CR11","unstructured":"Doberkat, E.E.: Basing Markov transition systems on the Giry monad (2008), \n                    \n                      http:\/\/www.informatics.sussex.ac.uk\/events\/domains9\/Slides\/Doberkat_GiryMonad.pdf"},{"key":"4_CR12","unstructured":"Eberl, M.: A Verified Compiler for Probability Density Functions. Master\u2019s thesis, Technische Universit\u00e4t M\u00fcnchen (2014), \n                    \n                      https:\/\/in.tum.de\/~eberlm\/pdfcompiler.pdf"},{"key":"4_CR13","doi-asserted-by":"crossref","unstructured":"Eberl, M., H\u00f6lzl, J., Nipkow, T.: A verified compiler for probability density functions. Archive of Formal Proofs, Formal proof development (October 2014), \n                    \n                      http:\/\/afp.sf.net\/entries\/Density_Compiler.shtml\n                    \n                    \n                  ,","DOI":"10.1007\/978-3-662-46669-8_4"},{"key":"4_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"68","DOI":"10.1007\/BFb0092872","volume-title":"TAPSOFT \u201995: Theory and Practice of Software Development","author":"M. Giry","year":"1995","unstructured":"Giry, M.: A categorical approach to probability theory. In: Mosses, P.D., Nielsen, M. (eds.) CAAP 1995, FASE 1995, and TAPSOFT 1995. LNCS, vol.\u00a0915, pp. 68\u201385. Springer, Heidelberg (1995), \n                    \n                      http:\/\/dx.doi.org\/10.1007\/BFb0092872\n                    \n                    \n                  , doi:10.1007\/BFb0092872"},{"key":"4_CR15","unstructured":"H\u00f6lzl, J.: Construction and stochastic applications of measure spaces in Higher-Order Logic. PhD thesis, Technische Universit\u00e4t M\u00fcnchen, Institut f\u00fcr Informatik (2012)"},{"key":"4_CR16","unstructured":"Hurd, J.: Formal Verification of Probabilistic Algorithms. Ph.D. thesis, University of Cambridge (2002)"},{"key":"4_CR17","doi-asserted-by":"publisher","first-page":"95","DOI":"10.1016\/j.entcs.2004.01.021","volume":"112","author":"J. Hurd","year":"2005","unstructured":"Hurd, J., McIver, A., Morgan, C.: Probabilistic guarded commands mechanized in HOL. Electron. Notes Theor. Comput. Sci.\u00a0112, 95\u2013111 (2005), \n                    \n                      http:\/\/dx.doi.org\/10.1016\/j.entcs.2004.01.021","journal-title":"Electron. Notes Theor. Comput. Sci."},{"key":"4_CR18","doi-asserted-by":"crossref","unstructured":"Nipkow, T., Klein, G.: Concrete Semantics with Isabelle\/HOL. Springer (2014), \n                    \n                      http:\/\/www.concrete-semantics.org","DOI":"10.1007\/978-3-319-10542-0"},{"key":"4_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL \u2014 A Proof Assistant for Higher-Order Logic","author":"T. Nipkow","year":"2002","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle\/HOL. LNCS, vol.\u00a02283. Springer, Heidelberg (2002)"},{"key":"4_CR20","first-page":"171","volume-title":"Proceedings of the 32Nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2005","author":"S. Park","year":"2005","unstructured":"Park, S., Pfenning, F., Thrun, S.: A probabilistic language based upon sampling functions. In: Proceedings of the 32Nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2005, pp. 171\u2013182. ACM, New York (2005), \n                    \n                      http:\/\/doi.acm.org\/10.1145\/1040305.1040320"},{"key":"4_CR21","doi-asserted-by":"publisher","first-page":"327","DOI":"10.1007\/s10817-008-9097-2","volume":"40","author":"C. Urban","year":"2008","unstructured":"Urban, C.: Nominal techniques in Isabelle\/HOL. Journal of Automated Reasoning\u00a040, 327\u2013356 (2008)","journal-title":"Journal of Automated Reasoning"}],"container-title":["Lecture Notes in Computer Science","Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-662-46669-8_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,29]],"date-time":"2019-05-29T14:27:53Z","timestamp":1559140073000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-662-46669-8_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783662466681","9783662466698"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/978-3-662-46669-8_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015]]}}}