{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:16:07Z","timestamp":1750220167833,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":33,"publisher":"ACM","license":[{"start":{"date-parts":[[2022,10,6]],"date-time":"2022-10-06T00:00:00Z","timestamp":1665014400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"FAPEMIG - Funda\u00e7\u00e3o de Amparo a Pesquisa de Minas Gerais","award":["APQ-01683-21"],"award-info":[{"award-number":["APQ-01683-21"]}]},{"name":"FAPESC - Funda\u00e7\u00e3o de Amparo a Pesquisa de Santa Catarina","award":["2021TR961"],"award-info":[{"award-number":["2021TR961"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2022,10,6]]},"DOI":"10.1145\/3561320.3561329","type":"proceedings-article","created":{"date-parts":[[2022,9,26]],"date-time":"2022-09-26T22:11:32Z","timestamp":1664230292000},"page":"1-7","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["A Sound Deep Embedding of Arbitrary Normal Modal Logics in Coq"],"prefix":"10.1145","author":[{"given":"Ariel Agne","family":"Da Silveira","sequence":"first","affiliation":[{"name":"Universidade Federal de Ouro Preto, Brazil"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Rodrigo","family":"Ribeiro","sequence":"additional","affiliation":[{"name":"Universidade Federal de Ouro Preto, Brazil"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Miguel Alfredo","family":"Nunes","sequence":"additional","affiliation":[{"name":"Universidade do Estado de Santa Catarina, Brazil"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Paulo","family":"Torrens","sequence":"additional","affiliation":[{"name":"Universidade do Estado de Santa Catarina, Brazil"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Karina","family":"Roggia","sequence":"additional","affiliation":[{"name":"Universidade do Estado de Santa Catarina, Brazil"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2022,10,6]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/1190216.1190235"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-89391-0_25"},{"volume-title":"Computer Science \u2013 Theory and Applications, Lev\u00a0D","author":"Benzm\u00fcller Christoph","key":"e_1_3_2_1_3_1","unstructured":"Christoph Benzm\u00fcller and Bruno Woltzenlogel\u00a0Paleo . 2015. Interacting with Modal Logics in the Coq Proof Assistant . In Computer Science \u2013 Theory and Applications, Lev\u00a0D . Beklemishev and Daniil\u00a0V. Musatov (Eds.). Springer International Publishing , Cham , 398\u2013411. Christoph Benzm\u00fcller and Bruno Woltzenlogel\u00a0Paleo. 2015. Interacting with Modal Logics in the Coq Proof Assistant. In Computer Science \u2013 Theory and Applications, Lev\u00a0D. Beklemishev and Daniil\u00a0V. Musatov (Eds.). Springer International Publishing, Cham, 398\u2013411."},{"key":"e_1_3_2_1_4_1","volume-title":"Interactive Theorem Proving and Program Development: Coq\u2019Art The Calculus of Inductive Constructions","author":"Bertot Yves","unstructured":"Yves Bertot and Pierre Castran . 2010. Interactive Theorem Proving and Program Development: Coq\u2019Art The Calculus of Inductive Constructions ( 1 st ed.). Springer Publishing Company, Inc orporated. Yves Bertot and Pierre Castran. 2010. Interactive Theorem Proving and Program Development: Coq\u2019Art The Calculus of Inductive Constructions(1st ed.). Springer Publishing Company, Incorporated.","edition":"1"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"crossref","unstructured":"P. Blackburn M. de Rijke and Y. Venema. 2001. Modal Logic. Cambridge University Press New York NY USA.  P. Blackburn M. de Rijke and Y. Venema. 2001. Modal Logic. Cambridge University Press New York NY USA.","DOI":"10.1017\/CBO9781107050884"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781107050884"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511625183"},{"volume-title":"Modal logic: an introduction","author":"Chellas F","key":"e_1_3_2_1_8_1","unstructured":"Brian\u00a0 F Chellas . 1980. Modal logic: an introduction . Cambridge University Press . Brian\u00a0F Chellas. 1980. Modal logic: an introduction. Cambridge University Press."},{"volume-title":"Certified Programming with Dependent Types: A Pragmatic Introduction to the Coq Proof Assistant","author":"Chlipala Adam","key":"e_1_3_2_1_9_1","unstructured":"Adam Chlipala . 2013. Certified Programming with Dependent Types: A Pragmatic Introduction to the Coq Proof Assistant . The MIT Press . Adam Chlipala. 2013. Certified Programming with Dependent Types: A Pragmatic Introduction to the Coq Proof Assistant. The MIT Press."},{"key":"e_1_3_2_1_10_1","unstructured":"Paulien de Wind. 2001. Modal logic in coq. Master\u2019s thesis. Vrije Universiteit.  Paulien de Wind. 2001. Modal logic in coq. Master\u2019s thesis. Vrije Universiteit."},{"key":"e_1_3_2_1_11_1","unstructured":"The\u00a0Coq development team. 2019. The Coq proof assistant reference manual. LogiCal Project. http:\/\/coq.inria.frVersion 8.9.0.  The\u00a0Coq development team. 2019. The Coq proof assistant reference manual. LogiCal Project. http:\/\/coq.inria.frVersion 8.9.0."},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2008.10.002"},{"key":"e_1_3_2_1_14_1","volume-title":"21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning. EasyChair, 14\u201330","author":"Glei\u00dfner Tobias","year":"2017","unstructured":"Tobias Glei\u00dfner , Alexander Steen , and Christoph Benzm\u00fcller . 2017 . Theorem provers for every normal modal logic. In LPAR-21 . 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning. EasyChair, 14\u201330 . Tobias Glei\u00dfner, Alexander Steen, and Christoph Benzm\u00fcller. 2017. Theorem provers for every normal modal logic. In LPAR-21. 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning. EasyChair, 14\u201330."},{"key":"e_1_3_2_1_15_1","volume-title":"Eine Interpretation des intuitionistischen Aussagenkalkuls. Ergebnisse eines Mathematischen Kolloquiums 4","author":"G\u00f6del K.","year":"1933","unstructured":"K. G\u00f6del . 1933. Eine Interpretation des intuitionistischen Aussagenkalkuls. Ergebnisse eines Mathematischen Kolloquiums 4 ( 1933 ), 34\u201340. K. G\u00f6del. 1933. Eine Interpretation des intuitionistischen Aussagenkalkuls. Ergebnisse eines Mathematischen Kolloquiums 4 (1933), 34\u201340."},{"volume-title":"Mathematics of Modality","author":"Goldblatt R.","key":"e_1_3_2_1_16_1","unstructured":"R. Goldblatt . 1993. Mathematics of Modality . CSLI Publications , Stanford, California . R. Goldblatt. 1993. Mathematics of Modality. CSLI Publications, Stanford, California."},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-87827-8_28"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39634-2_14"},{"key":"e_1_3_2_1_19_1","unstructured":"G.\u00a0A. Kavvos. 2016. The Many Worlds of Modal \u03bb-calculi: I. Curry-Howard for Necessity Possibility and Time. CoRR abs\/1605.08106(2016). arXiv:1605.08106http:\/\/arxiv.org\/abs\/1605.08106  G.\u00a0A. Kavvos. 2016. The Many Worlds of Modal \u03bb-calculi: I. Curry-Howard for Necessity Possibility and Time. CoRR abs\/1605.08106(2016). arXiv:1605.08106http:\/\/arxiv.org\/abs\/1605.08106"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/1743546.1743574"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/1538788.1538814"},{"volume-title":"A Survey of Symbolic Logic","author":"Lewis I.","key":"e_1_3_2_1_22_1","unstructured":"C.\u00a0 I. Lewis . 1918. A Survey of Symbolic Logic . University of California Press , Berkeley and Los Angeles. C.\u00a0I. Lewis. 1918. A Survey of Symbolic Logic. University of California Press, Berkeley and Los Angeles."},{"key":"e_1_3_2_1_23_1","volume-title":"Symbolic Logic","author":"Lewis I.","year":"1959","unstructured":"C.\u00a0 I. Lewis and C.\u00a0 H. Langford . 1932. Symbolic Logic . The Century Company. 2 nd ed. 1959 , Dover Publications , Inc. C.\u00a0I. Lewis and C.\u00a0H. Langford. 1932. Symbolic Logic. The Century Company. 2nd ed. 1959, Dover Publications, Inc.","edition":"2"},{"key":"e_1_3_2_1_24_1","unstructured":"Marco Maggesi and Cosimo\u00a0Perini Brogi. 2021. A formal proof of modal completeness for provability logic. CoRR abs\/2102.05945(2021). arXiv:2102.05945https:\/\/arxiv.org\/abs\/2102.05945  Marco Maggesi and Cosimo\u00a0Perini Brogi. 2021. A formal proof of modal completeness for provability logic. CoRR abs\/2102.05945(2021). arXiv:2102.05945https:\/\/arxiv.org\/abs\/2102.05945"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/3372885.3373824"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1111\/j.1755-2567.1970.tb00434.x"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1080\/00207160.2010.493211"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2004.1319623"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-10542-0"},{"key":"e_1_3_2_1_30_1","volume-title":"A Proof Assistant for Higher-Order Logic","author":"Nipkow Tobias","year":"2019","unstructured":"Tobias Nipkow , Lawrence\u00a0 C. Paulson , and Markus Wenzel . 2019. A Proof Assistant for Higher-Order Logic . Springer-Verlag . https:\/\/isabelle.in.tum.de\/documentation.htmlIsabelle 2019 . Tobias Nipkow, Lawrence\u00a0C. Paulson, and Markus Wenzel. 2019. A Proof Assistant for Higher-Order Logic. Springer-Verlag. https:\/\/isabelle.in.tum.de\/documentation.htmlIsabelle2019."},{"volume-title":"All about Proofs, Proofs for All, Bruno\u00a0Woltzenlogel Paleo and David Delahaye (Eds.). Studies in Logic (Mathematical logic and foundations), Vol.\u00a055","author":"Paulin-Mohring Christine","key":"e_1_3_2_1_31_1","unstructured":"Christine Paulin-Mohring . 2015. Introduction to the Calculus of Inductive Constructions . In All about Proofs, Proofs for All, Bruno\u00a0Woltzenlogel Paleo and David Delahaye (Eds.). Studies in Logic (Mathematical logic and foundations), Vol.\u00a055 . College Publications . https:\/\/hal.inria.fr\/hal-01094195 Christine Paulin-Mohring. 2015. Introduction to the Calculus of Inductive Constructions. In All about Proofs, Proofs for All, Bruno\u00a0Woltzenlogel Paleo and David Delahaye (Eds.). Studies in Logic (Mathematical logic and foundations), Vol.\u00a055. College Publications. https:\/\/hal.inria.fr\/hal-01094195"},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1109\/SFCS.1976.27"},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF00370324"},{"volume-title":"Philosophical Problems in Logic, K.\u00a0Lambert (Ed.)","author":"Scott D.","key":"e_1_3_2_1_34_1","unstructured":"D. Scott . 1970. Advice on modal logic . In Philosophical Problems in Logic, K.\u00a0Lambert (Ed.) . Reidel , Dordrecht , 143\u2013173. D. Scott. 1970. Advice on modal logic. In Philosophical Problems in Logic, K.\u00a0Lambert (Ed.). Reidel, Dordrecht, 143\u2013173."}],"event":{"name":"SBLP 2022: XXVI Brazilian Symposium on Programming Languages","acronym":"SBLP 2022","location":"Virtual Event Brazil"},"container-title":["Proceedings of the XXVI Brazilian Symposium on Programming Languages"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3561320.3561329","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3561320.3561329","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T19:00:35Z","timestamp":1750186835000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3561320.3561329"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,10,6]]},"references-count":33,"alternative-id":["10.1145\/3561320.3561329","10.1145\/3561320"],"URL":"https:\/\/doi.org\/10.1145\/3561320.3561329","relation":{},"subject":[],"published":{"date-parts":[[2022,10,6]]},"assertion":[{"value":"2022-10-06","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}