{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,14]],"date-time":"2026-03-14T22:22:40Z","timestamp":1773526960528,"version":"3.50.1"},"reference-count":55,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2019,1,2]],"date-time":"2019-01-02T00:00:00Z","timestamp":1546387200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/501100002347","name":"Bundesministerium f\u00fcr Bildung und Forschung","doi-asserted-by":"publisher","award":["01IS160253"],"award-info":[{"award-number":["01IS160253"]}],"id":[{"id":"10.13039\/501100002347","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100000266","name":"Engineering and Physical Sciences Research Council","doi-asserted-by":"publisher","award":["EP\/P020909\/1"],"award-info":[{"award-number":["EP\/P020909\/1"]}],"id":[{"id":"10.13039\/501100000266","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100001840","name":"Icelandic Centre for Research","doi-asserted-by":"publisher","award":["163406-051, 184940-051"],"award-info":[{"award-number":["163406-051, 184940-051"]}],"id":[{"id":"10.13039\/501100001840","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2019,1,2]]},"abstract":"<jats:p>This paper establishes a comprehensive theory of runtime monitorability for Hennessy-Milner logic with recursion, a very expressive variant of the modal \u00b5-calculus. It investigates the monitorability of that logic with a linear-time semantics and then compares the obtained results with ones that were previously presented in the literature for a branching-time setting. Our work establishes an expressiveness hierarchy of monitorable fragments of Hennessy-Milner logic with recursion in a linear-time setting and exactly identifies what kinds of guarantees can be given using runtime monitors for each fragment in the hierarchy. Each fragment is shown to be complete, in the sense that it can express all properties that can be monitored under the corresponding guarantees. The study is carried out using a principled approach to monitoring that connects the semantics of the logic and the operational semantics of monitors. The proposed framework supports the automatic, compositional synthesis of correct monitors from monitorable properties.<\/jats:p>","DOI":"10.1145\/3290365","type":"journal-article","created":{"date-parts":[[2019,1,4]],"date-time":"2019-01-04T13:33:51Z","timestamp":1546608831000},"page":"1-29","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":38,"title":["Adventures in monitorability: from branching to linear time and back again"],"prefix":"10.1145","volume":"3","author":[{"given":"Luca","family":"Aceto","sequence":"first","affiliation":[{"name":"Gran Sasso Science Institute, Iceland \/ Reykjavik University, Iceland"}]},{"given":"Antonis","family":"Achilleos","sequence":"additional","affiliation":[{"name":"Reykjavik University, Iceland"}]},{"given":"Adrian","family":"Francalanza","sequence":"additional","affiliation":[{"name":"University of Malta, Malta"}]},{"given":"Anna","family":"Ing\u00f3lfsd\u00f3ttir","sequence":"additional","affiliation":[{"name":"Reykjavik University, Iceland"}]},{"given":"Karoliina","family":"Lehtinen","sequence":"additional","affiliation":[{"name":"University of Kiel, Germany \/ University of Liverpool, UK"}]}],"member":"320","published-online":{"date-parts":[[2019,1,2]]},"reference":[{"key":"e_1_2_2_1_1","first-page":"1","article-title":"Monitoring for silent actions. In FSTTCS (LIPIcs) , Satya Lokam and R. Ramanujam (Eds.), Vol. 93. Schloss Dagstuhl\u2013Leibniz-Zentrum fuer Informatik, Dagstuhl","volume":"7","author":"Aceto Luca","year":"2017","unstructured":"Luca Aceto , Antonis Achilleos , Adrian Francalanza , and Anna Ing\u00f3lfsd\u00f3ttir . 2017 a. Monitoring for silent actions. In FSTTCS (LIPIcs) , Satya Lokam and R. Ramanujam (Eds.), Vol. 93. Schloss Dagstuhl\u2013Leibniz-Zentrum fuer Informatik, Dagstuhl , Germany , 7 : 1 \u2013 7 :14. Luca Aceto, Antonis Achilleos, Adrian Francalanza, and Anna Ing\u00f3lfsd\u00f3ttir. 2017a. Monitoring for silent actions. In FSTTCS (LIPIcs) , Satya Lokam and R. Ramanujam (Eds.), Vol. 93. Schloss Dagstuhl\u2013Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany, 7:1\u20137:14.","journal-title":"Germany"},{"key":"e_1_2_2_2_1","volume-title":"FOSSACS (Lecture Notes in Computer Science)","author":"Aceto Luca","unstructured":"Luca Aceto , Antonis Achilleos , Adrian Francalanza , and Anna Ing\u00f3lfsd\u00f3ttir . 2018a. A Framework for Parametrized Monitorability . In FOSSACS (Lecture Notes in Computer Science) , Vol. 10803 . Springer , 203\u2013220. Luca Aceto, Antonis Achilleos, Adrian Francalanza, and Anna Ing\u00f3lfsd\u00f3ttir. 2018a. A Framework for Parametrized Monitorability. In FOSSACS (Lecture Notes in Computer Science), Vol. 10803. Springer, 203\u2013220."},{"key":"e_1_2_2_3_1","volume-title":"Determinizing Monitors for HML with Recursion. CoRR abs\/1611.10212","author":"Aceto Luca","year":"2016","unstructured":"Luca Aceto , Antonis Achilleos , Adrian Francalanza , Anna Ing\u00f3lfsd\u00f3ttir , and S\u00e6var \u00d6rn Kjartansson . 2016. Determinizing Monitors for HML with Recursion. CoRR abs\/1611.10212 ( 2016 ). arXiv: 1611.10212 http:\/\/arxiv.org\/abs\/1611.10212 Luca Aceto, Antonis Achilleos, Adrian Francalanza, Anna Ing\u00f3lfsd\u00f3ttir, and S\u00e6var \u00d6rn Kjartansson. 2016. Determinizing Monitors for HML with Recursion. CoRR abs\/1611.10212 (2016). arXiv: 1611.10212 http:\/\/arxiv.org\/abs\/1611.10212"},{"key":"e_1_2_2_4_1","volume-title":"Implementation and Application of Automata","author":"Aceto Luca","unstructured":"Luca Aceto , Antonis Achilleos , Adrian Francalanza , Anna Ing\u00f3lfsd\u00f3ttir , and S\u00e6var \u00d6rn Kjartansson . 2017b. On the Complexity of Determinizing Monitors . In Implementation and Application of Automata . Springer International Publishing , 1\u201313. Luca Aceto, Antonis Achilleos, Adrian Francalanza, Anna Ing\u00f3lfsd\u00f3ttir, and S\u00e6var \u00d6rn Kjartansson. 2017b. On the Complexity of Determinizing Monitors. In Implementation and Application of Automata. Springer International Publishing, 1\u201313."},{"key":"e_1_2_2_5_1","volume-title":"CONCUR (LIPIcs)","volume":"118","author":"Aceto Luca","year":"2018","unstructured":"Luca Aceto , Ian Cassar , Adrian Francalanza , and Anna Ing\u00f3lfsd\u00f3ttir . 2018 b. On Runtime Enforcement via Suppressions . In CONCUR (LIPIcs) , Vol. 118 . Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 34:1\u201334:17. Luca Aceto, Ian Cassar, Adrian Francalanza, and Anna Ing\u00f3lfsd\u00f3ttir. 2018b. On Runtime Enforcement via Suppressions. In CONCUR (LIPIcs) , Vol. 118. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 34:1\u201334:17."},{"key":"e_1_2_2_6_1","volume-title":"Kim Guldstrand Larsen, and Jiri Srba","author":"Aceto Luca","year":"2007","unstructured":"Luca Aceto , Anna Ing\u00f3lfsd\u00f3ttir , Kim Guldstrand Larsen, and Jiri Srba . 2007 . Reactive Systems : Modelling, Specification and Verification . Cambridge Univ. Press , New York, NY, USA. Luca Aceto, Anna Ing\u00f3lfsd\u00f3ttir, Kim Guldstrand Larsen, and Jiri Srba. 2007. Reactive Systems: Modelling, Specification and Verification . Cambridge Univ. Press, New York, NY, USA."},{"key":"e_1_2_2_7_1","volume-title":"Logical Foundations of Computer Science","author":"Achilleos Antonis","unstructured":"Antonis Achilleos . 2016. Modal Logics with Hard Diamond-Free Fragments . In Logical Foundations of Computer Science , Sergei Artemov and Anil Nerode (Eds.). Springer International Publishing , Cham , 1\u201313. Antonis Achilleos. 2016. Modal Logics with Hard Diamond-Free Fragments. In Logical Foundations of Computer Science, Sergei Artemov and Anil Nerode (Eds.). Springer International Publishing, Cham, 1\u201313."},{"key":"e_1_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1016\/0020-0190(85)90056-0"},{"key":"e_1_2_2_9_1","volume-title":"Behavioural Types: from Theory to Tools","author":"Attard Duncan Paul","unstructured":"Duncan Paul Attard , Ian Cassar , Adrian Francalanza , Luca Aceto , and Anna Ingolfsdottir . 2017. Behavioural Types: from Theory to Tools . River Publishers , Chapter A Runtime Monitoring Tool for Actor-Based Systems, 49\u201374. Duncan Paul Attard, Ian Cassar, Adrian Francalanza, Luca Aceto, and Anna Ingolfsdottir. 2017. Behavioural Types: from Theory to Tools . River Publishers, Chapter A Runtime Monitoring Tool for Actor-Based Systems, 49\u201374."},{"key":"e_1_2_2_10_1","volume-title":"A Monitoring Tool for a Branching-Time Logic","author":"Attard Duncan Paul","unstructured":"Duncan Paul Attard and Adrian Francalanza . 2016. A Monitoring Tool for a Branching-Time Logic . Springer International Publishing , Cham , 473\u2013481. Duncan Paul Attard and Adrian Francalanza. 2016. A Monitoring Tool for a Branching-Time Logic. Springer International Publishing, Cham, 473\u2013481."},{"key":"e_1_2_2_11_1","volume-title":"Principles of model checking","author":"Baier Christel","unstructured":"Christel Baier , Joost-Pieter Katoen , and Kim Guldstrand Larsen . 2008. Principles of model checking . MIT press . Christel Baier, Joost-Pieter Katoen, and Kim Guldstrand Larsen. 2008. Principles of model checking. MIT press."},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24622-0_5"},{"key":"e_1_2_2_13_1","volume-title":"Introduction to Runtime Verification","author":"Bartocci Ezio","unstructured":"Ezio Bartocci , Yli\u00e8s Falcone , Adrian Francalanza , and Giles Reger . 2018. Introduction to Runtime Verification . Springer , 1\u201333. Ezio Bartocci, Yli\u00e8s Falcone, Adrian Francalanza, and Giles Reger. 2018. Introduction to Runtime Verification. Springer, 1\u201333."},{"key":"e_1_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/exn075"},{"key":"e_1_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/2000799.2000800"},{"key":"e_1_2_2_16_1","volume-title":"Foundation of Diagnosis and Predictability in Probabilistic Systems. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS\u201914)","author":"Bertrand Nathalie","year":"2014","unstructured":"Nathalie Bertrand , Serge Haddad , and Engel Lefaucheux . 2014 . Foundation of Diagnosis and Predictability in Probabilistic Systems. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS\u201914) . New Delhi, India. https:\/\/hal.inria.fr\/hal-01088117 Nathalie Bertrand, Serge Haddad, and Engel Lefaucheux. 2014. Foundation of Diagnosis and Predictability in Probabilistic Systems. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS\u201914). New Delhi, India. https:\/\/hal.inria.fr\/hal-01088117"},{"key":"e_1_2_2_17_1","volume-title":"Handbook of Process Algebra","author":"Bradfield Julian","unstructured":"Julian Bradfield and Colin Stirling . 2001. CHAPTER 4 - Modal Logics and mu-Calculi: An Introduction . In Handbook of Process Algebra , J.A. Bergstra, A. Ponse, and S.A. Smolka (Eds.). Elsevier Science , Amsterdam , 293 \u2013 330. Julian Bradfield and Colin Stirling. 2001. CHAPTER 4 - Modal Logics and mu-Calculi: An Introduction. In Handbook of Process Algebra , J.A. Bergstra, A. Ponse, and S.A. Smolka (Eds.). Elsevier Science, Amsterdam, 293 \u2013 330."},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/322234.322243"},{"key":"e_1_2_2_19_1","volume-title":"Automata, Languages and Properties (LNCS)","author":"Chang Edward","unstructured":"Edward Chang , Zohar Manna , and Amir Pnueli . 1992. Characterization of Temporal Property Classes . In Automata, Languages and Properties (LNCS) , Vol. 623 . Springer-Verlag , 474\u2013486. Edward Chang, Zohar Manna, and Amir Pnueli. 1992. Characterization of Temporal Property Classes. In Automata, Languages and Properties (LNCS) , Vol. 623. Springer-Verlag, 474\u2013486."},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46681-0_54"},{"key":"e_1_2_2_21_1","unstructured":"Edmund M Clarke Orna Grumberg and Doron Peled. 1999. Model Checking. MIT press.   Edmund M Clarke Orna Grumberg and Doron Peled. 1999. Model Checking. MIT press."},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1109\/TIME.2005.26"},{"key":"e_1_2_2_23_1","volume-title":"Semantics of Systems of Concurrent Processes , Ir\u00e8ne Guessarian (Ed.)","author":"Nicola Rocco De","unstructured":"Rocco De Nicola and Frits Vaandrager . 1990. Action versus state based logics for transition systems . In Semantics of Systems of Concurrent Processes , Ir\u00e8ne Guessarian (Ed.) . Springer Berlin Heidelberg , Berlin, Heidelberg , 407\u2013419. Rocco De Nicola and Frits Vaandrager. 1990. Action versus state based logics for transition systems. In Semantics of Systems of Concurrent Processes , Ir\u00e8ne Guessarian (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg, 407\u2013419."},{"key":"e_1_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2014.02.052"},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-25150-9_3"},{"key":"e_1_2_2_26_1","volume-title":"CAV","volume":"3","author":"Drusinsky Doron","year":"2003","unstructured":"Doron Drusinsky . 2003 . Monitoring temporal rules combined with time series . In CAV , Vol. 3 . Springer, 114\u2013118. Doron Drusinsky. 2003. Monitoring temporal rules combined with time series. In CAV, Vol. 3. Springer, 114\u2013118."},{"key":"e_1_2_2_27_1","volume-title":"Proceedings of the Second International Workshop on Design and Implementation of Formal Tools and Systems (CEUR Workshop Proceedings) , Malay K. Ganai and Alper Sen (Eds.)","volume":"1130","author":"Dutta Sonali","year":"2014","unstructured":"Sonali Dutta , Moshe Y. Vardi , and Deian Tabakov . 2014 . CHIMP: A Tool for Assertion-Based Dynamic Verification of SystemC Models . In Proceedings of the Second International Workshop on Design and Implementation of Formal Tools and Systems (CEUR Workshop Proceedings) , Malay K. Ganai and Alper Sen (Eds.) , Vol. 1130 . CEUR-WS.org. http: \/\/ceur-ws.org\/Vol-1130\/paper_8.pdf Sonali Dutta, Moshe Y. Vardi, and Deian Tabakov. 2014. CHIMP: A Tool for Assertion-Based Dynamic Verification of SystemC Models. In Proceedings of the Second International Workshop on Design and Implementation of Formal Tools and Systems (CEUR Workshop Proceedings) , Malay K. Ganai and Alper Sen (Eds.), Vol. 1130. CEUR-WS.org. http: \/\/ceur-ws.org\/Vol-1130\/paper_8.pdf"},{"key":"e_1_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-011-0196-8"},{"key":"e_1_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-011-0196-8"},{"key":"e_1_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1080\/00207169008803893"},{"key":"e_1_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1023\/B:FORM.0000017718.28096.48"},{"key":"e_1_2_2_32_1","first-page":"145","article-title":"A Theory of Monitors","volume":"9634","author":"Francalanza Adrian","year":"2016","unstructured":"Adrian Francalanza . 2016 . A Theory of Monitors . In FoSSaCS (LNCS) , Vol. 9634. 145 \u2013 161 . Adrian Francalanza. 2016. A Theory of Monitors. In FoSSaCS (LNCS), Vol. 9634. 145\u2013161.","journal-title":"FoSSaCS (LNCS)"},{"key":"e_1_2_2_33_1","first-page":"1","article-title":"Consistently-Detecting Monitors. In CONCUR (LIPIcs), Vol. 85. Schloss Dagstuhl, Dagstuhl","volume":"8","author":"Francalanza Adrian","year":"2017","unstructured":"Adrian Francalanza . 2017 . Consistently-Detecting Monitors. In CONCUR (LIPIcs), Vol. 85. Schloss Dagstuhl, Dagstuhl , Germany , 8 : 1 \u2013 8 :19. Adrian Francalanza. 2017. Consistently-Detecting Monitors. In CONCUR (LIPIcs), Vol. 85. Schloss Dagstuhl, Dagstuhl, Germany, 8:1\u20138:19.","journal-title":"Germany"},{"key":"e_1_2_2_34_1","volume-title":"Ian Cassar, Dario Della Monica, and Anna Ing\u00f3lfsd\u00f3ttir.","author":"Francalanza Adrian","year":"2017","unstructured":"Adrian Francalanza , Luca Aceto , Antonis Achilleos , Duncan Paul Attard , Ian Cassar, Dario Della Monica, and Anna Ing\u00f3lfsd\u00f3ttir. 2017 a. A Foundation for Runtime Monitoring. In RV. 8\u201329. Adrian Francalanza, Luca Aceto, Antonis Achilleos, Duncan Paul Attard, Ian Cassar, Dario Della Monica, and Anna Ing\u00f3lfsd\u00f3ttir. 2017a. A Foundation for Runtime Monitoring. In RV. 8\u201329."},{"key":"e_1_2_2_35_1","first-page":"71","article-title":"On Verifying Hennessy-Milner Logic with Recursion at Runtime","volume":"9333","author":"Francalanza Adrian","year":"2015","unstructured":"Adrian Francalanza , Luca Aceto , and Anna Ing\u00f3lfsd\u00f3ttir . 2015 . On Verifying Hennessy-Milner Logic with Recursion at Runtime . In RV (LNCS) , Vol. 9333. 71 \u2013 86 . Adrian Francalanza, Luca Aceto, and Anna Ing\u00f3lfsd\u00f3ttir. 2015. On Verifying Hennessy-Milner Logic with Recursion at Runtime. In RV (LNCS), Vol. 9333. 71\u201386.","journal-title":"RV (LNCS)"},{"key":"e_1_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-017-0273-z"},{"key":"e_1_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-014-0217-9"},{"key":"e_1_2_2_38_1","volume-title":"Proceedings of the 16th IEEE International Conference on Automated Software Engineering","author":"Giannakopoulou Dimitra","year":"2001","unstructured":"Dimitra Giannakopoulou and Klaus Havelund . 2001 . Runtime analysis of linear temporal logic specifications . In Proceedings of the 16th IEEE International Conference on Automated Software Engineering , San Diego, California . Dimitra Giannakopoulou and Klaus Havelund. 2001. Runtime analysis of linear temporal logic specifications. In Proceedings of the 16th IEEE International Conference on Automated Software Engineering, San Diego, California ."},{"key":"e_1_2_2_39_1","doi-asserted-by":"publisher","DOI":"10.5555\/646486.694486"},{"key":"e_1_2_2_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/2455.2460"},{"key":"e_1_2_2_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/360248.360251"},{"key":"e_1_2_2_42_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(82)90125-6"},{"key":"e_1_2_2_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/333979.333987"},{"key":"e_1_2_2_44_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30579-8_18"},{"key":"e_1_2_2_45_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(90)90038-J"},{"key":"e_1_2_2_46_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(91)90041-Y"},{"key":"e_1_2_2_47_1","doi-asserted-by":"publisher","DOI":"10.5555\/1138824.1711222"},{"key":"e_1_2_2_48_1","volume-title":"Communication and Concurrency","author":"Milner R.","unstructured":"R. Milner . 1989. Communication and Concurrency . Prentice-Hall . R. Milner. 1989. Communication and Concurrency. Prentice-Hall."},{"key":"e_1_2_2_49_1","doi-asserted-by":"publisher","DOI":"10.1007\/11813040_38"},{"key":"e_1_2_2_50_1","doi-asserted-by":"publisher","DOI":"10.1109\/9.412626"},{"key":"e_1_2_2_51_1","volume-title":"On Concurrent Programming","author":"Schneider Fred B.","unstructured":"Fred B. Schneider . 1997. On Concurrent Programming . Springer-Verlag . Fred B. Schneider. 1997. On Concurrent Programming. Springer-Verlag."},{"key":"e_1_2_2_52_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-011-0139-8"},{"key":"e_1_2_2_53_1","doi-asserted-by":"publisher","DOI":"10.1145\/73560.73582"},{"key":"e_1_2_2_54_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-31862-0_38"},{"key":"e_1_2_2_55_1","doi-asserted-by":"publisher","DOI":"10.36045\/bbms\/1102714178"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3290365","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3290365","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T00:58:04Z","timestamp":1750208284000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3290365"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,1,2]]},"references-count":55,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2019,1,2]]}},"alternative-id":["10.1145\/3290365"],"URL":"https:\/\/doi.org\/10.1145\/3290365","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019,1,2]]},"assertion":[{"value":"2019-01-02","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}