{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,10]],"date-time":"2026-02-10T19:26:47Z","timestamp":1770751607675,"version":"3.50.0"},"publisher-location":"Cham","reference-count":27,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032111753","type":"print"},{"value":"9783032111760","type":"electronic"}],"license":[{"start":{"date-parts":[[2025,11,23]],"date-time":"2025-11-23T00:00:00Z","timestamp":1763856000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2025,11,23]],"date-time":"2025-11-23T00:00:00Z","timestamp":1763856000000},"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":[[2026]]},"DOI":"10.1007\/978-3-032-11176-0_14","type":"book-chapter","created":{"date-parts":[[2025,11,22]],"date-time":"2025-11-22T20:11:27Z","timestamp":1763842287000},"page":"220-238","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["From Program Logics Towards Language Logics"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-0162-9997","authenticated-orcid":false,"given":"Matteo","family":"Cimini","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2025,11,23]]},"reference":[{"key":"14_CR1","doi-asserted-by":"publisher","unstructured":"Berghofer, S., Nipkow, T.: Random testing in Isabelle\/HOL. In: Proceedings of the 2nd International Conference on Software Engineering and Formal Methods, SEFM 2004, pp. 230\u2013239. IEEE Computer Society, USA (2004). https:\/\/doi.org\/10.1109\/SEFM.2004.10049","DOI":"10.1109\/SEFM.2004.10049"},{"key":"14_CR2","doi-asserted-by":"publisher","unstructured":"Brookes, S.: A semantics for concurrent separation logic. Theor. Comput. Sci. 375(1), 227\u2013270 (2007). https:\/\/doi.org\/10.1016\/j.tcs.2006.12.034","DOI":"10.1016\/j.tcs.2006.12.034"},{"key":"14_CR3","doi-asserted-by":"publisher","unstructured":"Chargu\u00e9raud, A.: Program verification through characteristic formulae. In: Proceedings of the 15th ACM SIGPLAN International Conference on Functional Programming, ICFP 2010, pp. 321\u2013332. ACM, New York (2010). https:\/\/doi.org\/10.1145\/1863543.1863590","DOI":"10.1145\/1863543.1863590"},{"key":"14_CR4","doi-asserted-by":"publisher","first-page":"56","DOI":"10.2307\/2266170","volume":"5","author":"A Church","year":"1940","unstructured":"Church, A.: A formulation of the simple theory of types. J. Symb. Log. 5, 56\u201368 (1940). https:\/\/doi.org\/10.2307\/2266170","journal-title":"J. Symb. Log."},{"key":"14_CR5","doi-asserted-by":"publisher","unstructured":"Cimini, M.: A calculus for multi-language operational semantics. In: Software Verification: 13th International Conference, VSTTE 2021, New Haven, CT, USA, 18\u201319 October 2021, and 14th International Workshop, NSV 2021, Los Angeles, CA, USA, 18\u201319 July 2021, pp. 25\u201342. Springer, Heidelberg (2021). https:\/\/doi.org\/10.1007\/978-3-030-95561-8_3","DOI":"10.1007\/978-3-030-95561-8_3"},{"key":"14_CR6","doi-asserted-by":"publisher","unstructured":"Cimini, M.: Lang-n-prove: A DSL for language proofs. In: Proceedings of the 15th ACM SIGPLAN International Conference on Software Language Engineering, SLE 2022, pp. 16\u201329. ACM, New York (2022). https:\/\/doi.org\/10.1145\/3567512.3567514","DOI":"10.1145\/3567512.3567514"},{"key":"14_CR7","doi-asserted-by":"publisher","unstructured":"Cimini, M.: Lang-n-send: processes that send languages. In: Carbone, M., Neykova, R. (eds.) Proceedings of the 13th International Workshop on Programming Language Approaches to Concurrency and Communication-cEntric Software, PLACES 2022, Munich, Germany, 3rd April 2022. EPTCS, vol.\u00a0356, pp. 46\u201356 (2022). https:\/\/doi.org\/10.4204\/EPTCS.356.5","DOI":"10.4204\/EPTCS.356.5"},{"key":"14_CR8","doi-asserted-by":"publisher","unstructured":"Cimini, M.: A query language for language analysis. In: Schlingloff, B., Chai, M. (eds.) Software Engineering and Formal Methods - 20th International Conference, SEFM 2022, Berlin, Germany, 26\u201330 September 2022, Proceedings. Lecture Notes in Computer Science, vol. 13550, pp. 57\u201373. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-031-17108-6_4","DOI":"10.1007\/978-3-031-17108-6_4"},{"key":"14_CR9","unstructured":"Cimini, M.: Lang-n-assert (2024). https:\/\/github.com\/mcimini\/lang-n-assert"},{"key":"14_CR10","doi-asserted-by":"publisher","unstructured":"Cimini, M., Miller, D., Siek, J.G.: Extrinsically typed operational semantics for functional languages. In: Proceedings of the 13th ACM SIGPLAN International Conference on Software Language Engineering, SLE 2020, Virtual Event, USA, 16\u201317 November 2020, pp. 108\u2013125 (2020). https:\/\/doi.org\/10.1145\/3426425.3426936","DOI":"10.1145\/3426425.3426936"},{"key":"14_CR11","doi-asserted-by":"publisher","unstructured":"Dijkstra, E.W.: Guarded commands, nondeterminacy and formal derivation of programs. Commun. ACM 18(8), 453\u2013457 (1975). https:\/\/doi.org\/10.1145\/360933.360975","DOI":"10.1145\/360933.360975"},{"key":"14_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"383","DOI":"10.1007\/978-3-662-46669-8_16","volume-title":"Programming Languages and Systems","author":"B Fetscher","year":"2015","unstructured":"Fetscher, B., Claessen, K., Pa\u0142ka, M., Hughes, J., Findler, R.B.: Making random judgments: automatically generating well-typed terms from the definition of a type-system. In: Vitek, J. (ed.) ESOP 2015. LNCS, vol. 9032, pp. 383\u2013405. Springer, Heidelberg (2015). https:\/\/doi.org\/10.1007\/978-3-662-46669-8_16"},{"key":"14_CR13","doi-asserted-by":"publisher","unstructured":"Galasso, S., Cimini, M.: Language-parameterized proofs for functional languages with subtyping. In: Gibbons, J., Miller, D. (eds.) Functional and Logic Programming - 17th International Symposium, FLOPS 2024, Proceedings. pp. 291\u2013310 (2024). https:\/\/doi.org\/10.1007\/978-981-97-2300-3_15","DOI":"10.1007\/978-981-97-2300-3_15"},{"issue":"1","key":"14_CR14","doi-asserted-by":"publisher","first-page":"95","DOI":"10.1145\/147508.147524","volume":"39","author":"JA Goguen","year":"1992","unstructured":"Goguen, J.A., Burstall, R.M.: Institutions: abstract model theory for specification and programming. J. ACM (JACM) 39(1), 95\u2013146 (1992). https:\/\/doi.org\/10.1145\/147508.147524","journal-title":"J. ACM (JACM)"},{"key":"14_CR15","doi-asserted-by":"publisher","unstructured":"Grewe, S., Erdweg, S., Wittmann, P., Mezini, M.: Type systems for the masses: deriving soundness proofs and efficient checkers. In: 2015 ACM International Symposium on New Ideas, New Paradigms, and Reflections on Programming and Software (Onward!), Onward! 2015, pp. 137\u2013150. ACM, New York (2015). https:\/\/doi.org\/10.1145\/2814228.2814239","DOI":"10.1145\/2814228.2814239"},{"key":"14_CR16","doi-asserted-by":"publisher","unstructured":"Hoare, C.A.R.: An axiomatic basis for computer programming. Commun. ACM 12(10), 576\u2013580 (1969). https:\/\/doi.org\/10.1145\/363235.363259","DOI":"10.1145\/363235.363259"},{"key":"14_CR17","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139021326","volume-title":"Programming with Higher-Order Logic","author":"D Miller","year":"2012","unstructured":"Miller, D., Nadathur, G.: Programming with Higher-Order Logic, 1st edn. Cambridge University Press, New York (2012)","edition":"1"},{"issue":"3","key":"14_CR18","doi-asserted-by":"publisher","first-page":"238","DOI":"10.1016\/j.tcs.2006.12.019","volume":"373","author":"MR Mousavi","year":"2007","unstructured":"Mousavi, M.R., Reniers, M.A., Groote, J.F.: SOS formats and meta-theory: 20 years after. Theoret. Comput. Sci. 373(3), 238\u2013272 (2007). https:\/\/doi.org\/10.1016\/j.tcs.2006.12.019","journal-title":"Theoret. Comput. Sci."},{"key":"14_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/3-540-44802-0_1","volume-title":"Computer Science Logic","author":"P O\u2019Hearn","year":"2001","unstructured":"O\u2019Hearn, P., Reynolds, J., Yang, H.: Local reasoning about programs that alter data structures. In: Fribourg, L. (ed.) CSL 2001. LNCS, vol. 2142, pp. 1\u201319. Springer, Heidelberg (2001). https:\/\/doi.org\/10.1007\/3-540-44802-0_1"},{"key":"14_CR20","doi-asserted-by":"publisher","unstructured":"O\u2019Hearn, P.W.: Resources, concurrency, and local reasoning. Theor. Comput. Sci. 375(1), 271\u2013307 (2007). https:\/\/doi.org\/10.1016\/j.tcs.2006.12.035","DOI":"10.1016\/j.tcs.2006.12.035"},{"key":"14_CR21","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"202","DOI":"10.1007\/3-540-48660-7_14","volume-title":"Automated Deduction \u2014 CADE-16","author":"F Pfenning","year":"1999","unstructured":"Pfenning, F., Sch\u00fcrmann, C.: System description: twelf \u2014 a meta-logical framework for deductive systems. In: CADE 1999. LNCS (LNAI), vol. 1632, pp. 202\u2013206. Springer, Heidelberg (1999). https:\/\/doi.org\/10.1007\/3-540-48660-7_14"},{"key":"14_CR22","unstructured":"Pierce, B.C.: Types and Programming Languages. MIT Press (2002)"},{"key":"14_CR23","doi-asserted-by":"publisher","unstructured":"Reynolds, J.C.: Separation logic: a logic for shared mutable data structures. In: Proceedings of the 17th Annual IEEE Symposium on Logic in Computer Science, LICS 2002, pp. 55\u201374. IEEE Computer Society, USA (2002). https:\/\/doi.org\/10.1109\/LICS.2002.1029817","DOI":"10.1109\/LICS.2002.1029817"},{"key":"14_CR24","doi-asserted-by":"publisher","unstructured":"Roberson, M., Harries, M., Darga, P.T., Boyapati, C.: Efficient software model checking of soundness of type systems. In: Harris, G.E. (ed.) Proceedings of the 23rd ACM SIGPLAN Conference on Object-Oriented Programming Systems Languages and Applications, OOPSLA 2008, pp. 493\u2013504. ACM, New York (2008). https:\/\/doi.org\/10.1145\/1449764.1449803","DOI":"10.1145\/1449764.1449803"},{"key":"14_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"357","DOI":"10.1007\/978-3-319-89884-1_13","volume-title":"Programming Languages and Systems","author":"K Svendsen","year":"2018","unstructured":"Svendsen, K., Pichon-Pharabod, J., Doko, M., Lahav, O., Vafeiadis, V.: A separation logic for a promising semantics. In: Ahmed, A. (ed.) ESOP 2018. LNCS, vol. 10801, pp. 357\u2013384. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-89884-1_13"},{"key":"14_CR26","doi-asserted-by":"publisher","unstructured":"Vafeiadis, V., Narayan, C.: Relaxed separation logic: a program logic for c11 concurrency. ACM SIGPLAN Not. 48(10), 867\u2013884 (2013). https:\/\/doi.org\/10.1145\/2544173.2509532","DOI":"10.1145\/2544173.2509532"},{"key":"14_CR27","doi-asserted-by":"publisher","unstructured":"Woodcock, J.: Hoare and He\u2019s Unifying Theories of Programming, 1 edn, pp. 285\u2013316. Association for Computing Machinery, New York (2021). https:\/\/doi.org\/10.1145\/3477355.3477369","DOI":"10.1145\/3477355.3477369"}],"container-title":["Lecture Notes in Computer Science","Theoretical Aspects of Computing \u2013 ICTAC 2025"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-032-11176-0_14","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,2,10]],"date-time":"2026-02-10T11:09:29Z","timestamp":1770721769000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-11176-0_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,11,23]]},"ISBN":["9783032111753","9783032111760"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-11176-0_14","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,11,23]]},"assertion":[{"value":"23 November 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"ICTAC","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Colloquium on Theoretical Aspects of Computing","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Marrakesh","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Morocco","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2025","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"24 November 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"28 November 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"22","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"ictac2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/ictac2025.digital-hub.sh\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}