{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,23]],"date-time":"2026-02-23T23:09:46Z","timestamp":1771888186661,"version":"3.50.1"},"publisher-location":"Cham","reference-count":22,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031765537","type":"print"},{"value":"9783031765544","type":"electronic"}],"license":[{"start":{"date-parts":[[2024,11,13]],"date-time":"2024-11-13T00:00:00Z","timestamp":1731456000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2024,11,13]],"date-time":"2024-11-13T00:00:00Z","timestamp":1731456000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2025]]},"DOI":"10.1007\/978-3-031-76554-4_7","type":"book-chapter","created":{"date-parts":[[2024,11,12]],"date-time":"2024-11-12T11:18:26Z","timestamp":1731410306000},"page":"109-127","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Stateful Functional Modeling with\u00a0Refinement (a Lean4 Framework)"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-4206-3283","authenticated-orcid":false,"given":"Fr\u00e9d\u00e9ric","family":"Peschanski","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2024,11,13]]},"reference":[{"key":"7_CR1","unstructured":"The focalize project. https:\/\/focalize.ensta-paris.fr\/"},{"key":"7_CR2","doi-asserted-by":"crossref","unstructured":"Abrial, J.: Modeling in Event-B - System and Software Engineering. Cambridge University Press (2010)","DOI":"10.1017\/CBO9781139195881"},{"key":"7_CR3","unstructured":"Baanen, A.: Use and abuse of instance parameters in the lean mathematical library. CoRR abs\/2202.01629 (2022). https:\/\/arxiv.org\/abs\/2202.01629"},{"key":"7_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"241","DOI":"10.1007\/978-3-031-63790-2_18","volume-title":"Rigorous State-Based Methods","author":"B Ballenghien","year":"2024","unstructured":"Ballenghien, B., Wolff, B.: Event-b as DSL in Isabelle and HOL experiences from a prototype. In: Bonfanti, S., Gargantini, A., Leuschel, M., Riccobene, E., Scandurra, P. (eds.) ABZ 2024. LNCS, vol. 14759, pp. 241\u2013247. Springer, Cham (2024). https:\/\/doi.org\/10.1007\/978-3-031-63790-2_18"},{"key":"7_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"350","DOI":"10.1007\/3-540-45648-1_18","volume-title":"ZB 2002:Formal Specification and Development in Z and B","author":"J-P Bodeveix","year":"2002","unstructured":"Bodeveix, J.-P., Filali, M.: Type synthesis in B and the translation of B to PVS. In: Bert, D., Bowen, J.P., Henson, M.C., Robinson, K. (eds.) ZB 2002. LNCS, vol. 2272, pp. 350\u2013369. Springer, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-45648-1_18"},{"key":"7_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). https:\/\/doi.org\/10.1007\/978-3-540-73228-0_6"},{"key":"7_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"66","DOI":"10.1007\/BFb0053356","volume-title":"B\u201998: Recent Advances in the Development and Use of the B Method","author":"P Chartier","year":"1998","unstructured":"Chartier, P.: Formalisation of B in Isabelle\/HOL. In: Bert, D. (ed.) B 1998. LNCS, vol. 1393, pp. 66\u201382. Springer, Heidelberg (1998). https:\/\/doi.org\/10.1007\/BFb0053356"},{"key":"7_CR8","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"135","DOI":"10.1007\/978-3-642-35786-2_11","volume-title":"Conceptual Structures for STEM Research and Education","author":"R Dapoigny","year":"2013","unstructured":"Dapoigny, R., Barlatier, P.: Modeling ontological structures with type classes in Coq. In: Pfeiffer, H.D., Ignatov, D.I., Poelmans, J., Gadiraju, N. (eds.) ICCS-ConceptStruct 2013. LNCS (LNAI), vol. 7735, pp. 135\u2013152. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-35786-2_11"},{"key":"7_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"31","DOI":"10.1007\/978-3-319-28934-2_2","volume-title":"Formal Aspects of Component Software","author":"D D\u00e9harbe","year":"2016","unstructured":"D\u00e9harbe, D., Merz, S.: Software component design with the b method\u2014a formalization in Isabelle\/HOL. In: Braga, C., \u00d6lveczky, P.C. (eds.) FACS 2015. LNCS, vol. 9539, pp. 31\u201347. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-28934-2_2"},{"key":"7_CR10","doi-asserted-by":"publisher","unstructured":"Hoang, T.S.: An introduction to the event-B modelling method. In: Hoang, T.S. (ed.) Industrial Deployment of System Engineering Methods, pp. 211\u2013236. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-33170-1","DOI":"10.1007\/978-3-642-33170-1"},{"issue":"1\u20133","key":"7_CR11","doi-asserted-by":"publisher","first-page":"67","DOI":"10.1016\/S0167-6423(99)00023-4","volume":"37","author":"J Hughes","year":"2000","unstructured":"Hughes, J.: Generalising monads to arrows. Sci. Comput. Program. 37(1\u20133), 67\u2013111 (2000)","journal-title":"Sci. Comput. Program."},{"key":"7_CR12","doi-asserted-by":"publisher","first-page":"88","DOI":"10.1007\/978-1-4471-3550-0_6","volume-title":"5th Refinement Workshop","author":"RB Jones","year":"1992","unstructured":"Jones, R.B.: Methods and tools for the verification of critical properties. In: Jones, C.B., Shaw, R.C., Denvir, T. (eds.) 5th Refinement Workshop, pp. 88\u2013118. Springer, London (1992). https:\/\/doi.org\/10.1007\/978-1-4471-3550-0_6"},{"key":"7_CR13","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"625","DOI":"10.1007\/978-3-030-79876-5_37","volume-title":"Automated Deduction \u2013 CADE 28","author":"L Moura","year":"2021","unstructured":"Moura, L., Ullrich, S.: The lean 4 theorem prover and programming language. In: Platzer, A., Sutcliffe, G. (eds.) CADE 2021. LNCS (LNAI), vol. 12699, pp. 625\u2013635. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-79876-5_37"},{"key":"7_CR14","doi-asserted-by":"crossref","unstructured":"Perone, M., Karachalias, G.: Cr\u00e8me de la crem: composable representable executable machines. In: Proceedings of the 1st ACM SIGPLAN International Workshop on Functional Software Architecture, pp. 11\u201319. Association for Computing Machinery (2023)","DOI":"10.1145\/3609025.3609480"},{"key":"7_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"462","DOI":"10.1007\/3-540-44659-1_29","volume-title":"Theorem Proving in Higher Order Logics","author":"R Pollack","year":"2000","unstructured":"Pollack, R.: Dependently typed records for representing mathematical structure. In: Aagaard, M., Harrison, J. (eds.) TPHOLs 2000. LNCS, vol. 1869, pp. 462\u2013479. Springer, Heidelberg (2000). https:\/\/doi.org\/10.1007\/3-540-44659-1_29"},{"key":"7_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"162","DOI":"10.1007\/978-3-030-77543-8_17","volume-title":"Rigorous State-Based Methods","author":"C Reynolds","year":"2021","unstructured":"Reynolds, C.: Formalizing the institution for event-B in\u00a0the Coq proof assistant. In: Raschke, A., M\u00e9ry, D. (eds.) ABZ 2021. LNCS, vol. 12709, pp. 162\u2013166. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-77543-8_17"},{"key":"7_CR17","doi-asserted-by":"crossref","unstructured":"Rivi\u00e8re, P., Singh, N.K., A\u00eft-Ameur, Y.: Eb4eb: a framework for reflexive event-b. In: 26th International Conference on Engineering of Complex Computer Systems (ICECCS), pp. 71\u201380 (2022)","DOI":"10.1109\/ICECCS54210.2022.00017"},{"key":"7_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"305","DOI":"10.1007\/978-3-030-32409-4_19","volume-title":"Formal Methods and Software Engineering","author":"BD Sall","year":"2019","unstructured":"Sall, B.D., Peschanski, F., Chailloux, E.: A mechanized theory of program refinement. In: Ait-Ameur, Y., Qin, S. (eds.) ICFEM 2019. LNCS, vol. 11852, pp. 305\u2013321. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-32409-4_19"},{"key":"7_CR19","unstructured":"Schmalz, M.: The logic of event-b. Technical report\u00a0698, ETH Z\u00fcrich (2011)"},{"key":"7_CR20","doi-asserted-by":"crossref","unstructured":"Ullrich, S., de\u00a0Moura, L.: Beyond notations: hygienic macro expansion for theorem proving languages. Log. Methods Comput. Sci. 18(2) (2022)","DOI":"10.46298\/lmcs-18(2:1)2022"},{"key":"7_CR21","doi-asserted-by":"crossref","unstructured":"Wadler, P., Blott, S.: How to make ad-hoc polymorphism less ad-hoc. In: Conference Record of the 16th ACM Symposium on Principles of Programming Languages, pp. 60\u201376. ACM Press (1989)","DOI":"10.1145\/75277.75283"},{"key":"7_CR22","unstructured":"Wlaschin, S.: Domain Modeling Made Functional. The Pragmatic Programmers (2018)"}],"container-title":["Lecture Notes in Computer Science","Integrated Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-76554-4_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,18]],"date-time":"2025-01-18T11:38:26Z","timestamp":1737200306000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-76554-4_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,11,13]]},"ISBN":["9783031765537","9783031765544"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-76554-4_7","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,11,13]]},"assertion":[{"value":"13 November 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"IFM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Integrated Formal Methods","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Manchester","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"United Kingdom","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2024","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"11 November 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"15 November 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"19","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"ifm2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/ifm2024.cs.manchester.ac.uk\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}