{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T11:01:58Z","timestamp":1770289318885,"version":"3.49.0"},"publisher-location":"Cham","reference-count":21,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319296036","type":"print"},{"value":"9783319296043","type":"electronic"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"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":[[2016]]},"DOI":"10.1007\/978-3-319-29604-3_3","type":"book-chapter","created":{"date-parts":[[2016,2,20]],"date-time":"2016-02-20T07:53:12Z","timestamp":1455954792000},"page":"29-44","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["From Proposition to Program"],"prefix":"10.1007","author":[{"given":"Wouter","family":"Swierstra","sequence":"first","affiliation":[]},{"given":"Joao","family":"Alpuim","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2016,2,21]]},"reference":[{"key":"3_CR1","doi-asserted-by":"crossref","unstructured":"Altenkirch, T., Morris, P.: Indexed containers. In: 24th Annual IEEE Symposium on Logic in Computer Science, LICS 2009, pp. 227\u2013285 (2009)","DOI":"10.1109\/LICS.2009.33"},{"key":"3_CR2","doi-asserted-by":"publisher","first-page":"247","DOI":"10.1007\/BF01888227","volume":"2","author":"RJR Back","year":"1989","unstructured":"Back, R.J.R., von Wright, J.: Refinement concepts formalized in higher order logic. Formal Aspects Comput. 2, 247\u2013272 (1989)","journal-title":"Formal Aspects Comput."},{"key":"3_CR3","series-title":"Texts in Computer Science","volume-title":"Refinement Calculus: Refinement Calculus","author":"J Wright Von","year":"1998","unstructured":"Von Wright, J.: Refinement Calculus: Refinement Calculus. Texts in Computer Science. Springer, New York (1998)"},{"issue":"1","key":"3_CR4","doi-asserted-by":"publisher","first-page":"247","DOI":"10.1007\/BF01888227","volume":"2","author":"RJR Back","year":"1990","unstructured":"Back, R.J.R., von Wright, J.: Refinement concepts formalised in higher order logic. Formal Aspects Comput. 2(1), 247\u2013272 (1990)","journal-title":"Formal Aspects Comput."},{"key":"3_CR5","unstructured":"Back, R.J.R.: On the Correctness of Refinement in Program Development. PhD thesis, University of Helsinki (1978)"},{"key":"3_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"54","DOI":"10.1007\/978-3-540-73228-0_6","volume-title":"Typed Lambda Calculi and Applications","author":"S Boulm\u00e9","year":"2007","unstructured":"Boulm\u00e9, S.: Intuitionistic refinement calculus. In: Della Rocca, S.R. (ed.) TLCA 2007. LNCS, vol. 4583, pp. 54\u201369. Springer, Heidelberg (2007)"},{"key":"3_CR7","unstructured":"Butler, M.J., Grundy, J., L\u00e5ngbacka, T., Ruksenas, R., Wright, J.V.: The refinement calculator. In: Formal Methods Pacific (1997)"},{"key":"3_CR8","doi-asserted-by":"crossref","unstructured":"Chlipala, A., Malecha, G., Morrisett, G., Shinnar, A., Wisnesky, R.: Effective interactive proofs for higher-order imperative programs. In: International Conference on Functional Programming, ICFP 2009, pp. 79\u201390 (2009)","DOI":"10.1145\/1631687.1596565"},{"key":"3_CR9","unstructured":"Dijkstra, E.W.: A Discipline of Programming. Prentice-Hall, Englewood Cliffs (1976)"},{"key":"3_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"137","DOI":"10.1007\/978-3-319-19797-5_7","volume-title":"Mathematics of Program Construction","author":"B Dongol","year":"2015","unstructured":"Dongol, B., Gomes, V.B.F., Struth, G.: A program construction and verification tool for separation logic. In: Hinze, R., Voigtl\u00e4nder, J. (eds.) MPC 2015. LNCS, vol. 9129, pp. 137\u2013158. Springer, Heidelberg (2015)"},{"issue":"19\u201332","key":"3_CR11","first-page":"1","volume":"19","author":"RW Floyd","year":"1967","unstructured":"Floyd, R.W.: Assigning meanings to programs. Math. Aspects Comput. Sci 19(19\u201332), 1 (1967)","journal-title":"Math. Aspects Comput. Sci"},{"issue":"1","key":"3_CR12","doi-asserted-by":"publisher","first-page":"189","DOI":"10.1016\/j.apal.2005.05.022","volume":"137","author":"P Hancock","year":"2006","unstructured":"Hancock, P., Hyvernat, P.: Programming interfaces and basic topology. Ann. Pure Appl. Logic 137(1), 189\u2013239 (2006)","journal-title":"Ann. Pure Appl. Logic"},{"key":"3_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"317","DOI":"10.1007\/3-540-44622-2_21","volume-title":"Computer Science Logic","author":"A Setzer","year":"2000","unstructured":"Setzer, A., Hancock, P.: Interactive programs in dependent type theory. In: Clote, P.G., Schwichtenberg, H. (eds.) CSL 2000. lncs, vol. 1862, pp. 317\u2013339. Springer, Heidelberg (2000)"},{"key":"3_CR14","unstructured":"Hancock, P., Setzer, A.: Specifying interactions with dependent types. In: Workshop on subtyping and dependent types in programming (2000b)"},{"issue":"10","key":"3_CR15","doi-asserted-by":"publisher","first-page":"576","DOI":"10.1145\/363235.363259","volume":"12","author":"CAR Hoare","year":"1969","unstructured":"Hoare, C.A.R.: An axiomatic basis for computer programming. Commun. ACM 12(10), 576\u2013580 (1969)","journal-title":"Commun. ACM"},{"key":"3_CR16","unstructured":"Morgan, C.: Programming from specifications. Prentice-Hall Inc, Upper Saddle River (1990)"},{"key":"3_CR17","doi-asserted-by":"crossref","unstructured":"Nanevski, A., Morrisett, G., Shinnar, A., Govereau, P., Birkedal, L.: Ynot: Dependent types for imperative programs. In: International Conference on Functional Programming, ICFP 2008, pp. 229\u2013240 (2008)","DOI":"10.1145\/1411203.1411237"},{"key":"3_CR18","volume-title":"Principles of Program Analysis","author":"N Flemming","year":"1999","unstructured":"Flemming, N., Nielson, H.R., Hankin, C.: Principles of Program Analysis. Springer, Heidelberg (1999)"},{"key":"3_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"440","DOI":"10.1007\/978-3-642-03359-9_30","volume-title":"Theorem Proving in Higher Order Logics","author":"W Swierstra","year":"2009","unstructured":"Swierstra, W.: A hoare logic for the state monad. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol. 5674, pp. 440\u2013451. Springer, Heidelberg (2009)"},{"key":"3_CR20","unstructured":"Swierstra, W.: A functional specification of effects. PhD thesis, University of Nottingham (2009)"},{"key":"3_CR21","doi-asserted-by":"crossref","unstructured":"Swierstra, W., Altenkirch, T.: Beauty in the beast: In: Proceedings of the ACM SIGPLAN Workshop on Haskell Workshop, pp. 25-36. ACM (2007)","DOI":"10.1145\/1291201.1291206"}],"container-title":["Lecture Notes in Computer Science","Functional and Logic Programming"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-29604-3_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,1,8]],"date-time":"2020-01-08T13:25:56Z","timestamp":1578489956000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-29604-3_3"}},"subtitle":["Embedding the Refinement Calculus in Coq"],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319296036","9783319296043"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-29604-3_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":"21 February 2016","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}