{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,13]],"date-time":"2025-12-13T23:10:13Z","timestamp":1765667413707,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":21,"publisher":"ACM","license":[{"start":{"date-parts":[[2022,9,20]],"date-time":"2022-09-20T00:00:00Z","timestamp":1663632000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["CCF-1617771"],"award-info":[{"award-number":["CCF-1617771"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2022,9,20]]},"DOI":"10.1145\/3551357.3551377","type":"proceedings-article","created":{"date-parts":[[2022,9,20]],"date-time":"2022-09-20T15:37:25Z","timestamp":1663688245000},"page":"1-13","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["A Logic for Formalizing Properties of LF Specifications"],"prefix":"10.1145","author":[{"given":"Gopalan","family":"Nadathur","sequence":"first","affiliation":[{"name":"University of Minnesota, United States"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mary","family":"Southern","sequence":"additional","affiliation":[{"name":"Amazon Web Services, United States"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2022,9,20]]},"reference":[{"key":"e_1_3_2_1_1_1","article-title":"Abella: A System for Reasoning about Relational Specifications","volume":"7","author":"Baelde David","year":"2014","unstructured":"David Baelde , Kaustuv Chaudhuri , Andrew Gacek , Dale Miller , Gopalan Nadathur , Alwen Tiu , and Yuting Wang . 2014 . Abella: A System for Reasoning about Relational Specifications . Journal of Formalized Reasoning 7 , 2 (2014). https:\/\/doi.org\/10.6092\/issn.1972-5787\/4650 10.6092\/issn.1972-5787 David Baelde, Kaustuv Chaudhuri, Andrew Gacek, Dale Miller, Gopalan Nadathur, Alwen Tiu, and Yuting Wang. 2014. Abella: A System for Reasoning about Relational Specifications. Journal of Formalized Reasoning 7, 2 (2014). https:\/\/doi.org\/10.6092\/issn.1972-5787\/4650","journal-title":"Journal of Formalized Reasoning"},{"volume-title":"A Framework for Specifying, Prototyping, and Reasoning about Computational Systems. Ph.\u00a0D. Dissertation","author":"Gacek Andrew","key":"e_1_3_2_1_2_1","unstructured":"Andrew Gacek . 2009. A Framework for Specifying, Prototyping, and Reasoning about Computational Systems. Ph.\u00a0D. Dissertation . University of Minnesota . Andrew Gacek. 2009. A Framework for Specifying, Prototyping, and Reasoning about Computational Systems. Ph.\u00a0D. Dissertation. University of Minnesota."},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2010.09.004"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796807006430"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1016\/0747-7171(92)90011-R"},{"key":"e_1_3_2_1_6_1","volume-title":"IEEE Symposium on Logic Programming, Seif Haridi (Ed.)","author":"Miller Dale","year":"1987","unstructured":"Dale Miller and Gopalan Nadathur . 1987 . A Logic Programming Approach to Manipulating Formulas and Programs . In IEEE Symposium on Logic Programming, Seif Haridi (Ed.) . San Francisco, 379\u2013388. Dale Miller and Gopalan Nadathur. 1987. A Logic Programming Approach to Manipulating Formulas and Programs. In IEEE Symposium on Logic Programming, Seif Haridi (Ed.). San Francisco, 379\u2013388."},{"volume-title":"Programming with Higher-Order Logic","author":"Miller Dale","key":"e_1_3_2_1_7_1","unstructured":"Dale Miller and Gopalan Nadathur . 2012. Programming with Higher-Order Logic . Cambridge University Press . https:\/\/doi.org\/10.1017\/CBO9781139021326 10.1017\/CBO9781139021326 Dale Miller and Gopalan Nadathur. 2012. Programming with Higher-Order Logic. Cambridge University Press. https:\/\/doi.org\/10.1017\/CBO9781139021326"},{"key":"e_1_3_2_1_8_1","volume-title":"A Logic for Reasoning About LF Specifications. (June","author":"Nadathur Gopalan","year":"2021","unstructured":"Gopalan Nadathur and Mary Southern . 2021. A Logic for Reasoning About LF Specifications. (June 2021 ). Available from http:\/\/arxiv.org\/abs\/2107.00111. . Gopalan Nadathur and Mary Southern. 2021. A Logic for Reasoning About LF Specifications. (June 2021). Available from http:\/\/arxiv.org\/abs\/2107.00111. ."},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/1352582.1352591"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/960116.54010"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-48660-7_14"},{"key":"e_1_3_2_1_12_1","unstructured":"Frank Pfenning and Carsten Sch\u00fcrmann. 2002. Twelf User\u2019s Guide. Available from http:\/\/www.cs.cmu.edu\/~twelf\/guide-1-4.  Frank Pfenning and Carsten Sch\u00fcrmann. 2002. Twelf User\u2019s Guide. Available from http:\/\/www.cs.cmu.edu\/~twelf\/guide-1-4."},{"key":"e_1_3_2_1_13_1","volume-title":"Cocon: Computation in Contextual Type Theory.","author":"Pientka Brigitte","year":"2019","unstructured":"Brigitte Pientka , Andreas Abel , Francisco Ferreira , David Thibodeau , and Rebecca Zucchini . 2019 . Cocon: Computation in Contextual Type Theory. (2019). Available from http:\/\/arxiv.org\/abs\/1901.03378. Brigitte Pientka, Andreas Abel, Francisco Ferreira, David Thibodeau, and Rebecca Zucchini. 2019. Cocon: Computation in Contextual Type Theory. (2019). Available from http:\/\/arxiv.org\/abs\/1901.03378."},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14203-1_2"},{"volume-title":"Types and Programming Languages","author":"Pierce C.","key":"e_1_3_2_1_15_1","unstructured":"Benjamin\u00a0 C. Pierce . 2002. Types and Programming Languages . MIT Press . Benjamin\u00a0C. Pierce. 2002. Types and Programming Languages. MIT Press."},{"volume-title":"Automating the Meta Theory of Deductive Systems. Ph.\u00a0D. Dissertation","author":"Sch\u00fcrmann Carsten","key":"e_1_3_2_1_16_1","unstructured":"Carsten Sch\u00fcrmann . 2000. Automating the Meta Theory of Deductive Systems. Ph.\u00a0D. Dissertation . Carnegie Mellon University . http:\/\/www.cs.yale.edu\/homes\/carsten\/papers\/S00b.ps.gz Carsten Sch\u00fcrmann. 2000. Automating the Meta Theory of Deductive Systems. Ph.\u00a0D. Dissertation. Carnegie Mellon University. http:\/\/www.cs.yale.edu\/homes\/carsten\/papers\/S00b.ps.gz"},{"volume-title":"A Framework for Reasoning About LF Specifications. Ph.\u00a0D. Dissertation","author":"Southern Mary","key":"e_1_3_2_1_17_1","unstructured":"Mary Southern . 2021. A Framework for Reasoning About LF Specifications. Ph.\u00a0D. Dissertation . University of Minnesota . https:\/\/conservancy.umn.edu\/handle\/11299\/223120 Mary Southern. 2021. A Framework for Reasoning About LF Specifications. Ph.\u00a0D. Dissertation. University of Minnesota. https:\/\/conservancy.umn.edu\/handle\/11299\/223120"},{"key":"e_1_3_2_1_18_1","volume-title":"34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014)(Leibniz International Proceedings in Informatics (LIPIcs), Vol.\u00a029)","author":"Southern Mary","year":"2014","unstructured":"Mary Southern and Kaustuv Chaudhuri . 2014 . A Two-Level Logic Approach to Reasoning About Typed Specification Languages . In 34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014)(Leibniz International Proceedings in Informatics (LIPIcs), Vol.\u00a029) , Venkatesh Raman and S.\u00a0P. Suresh (Eds.). Dagstuhl, Germany, 557\u2013569. https:\/\/doi.org\/10.4230\/LIPIcs.FSTTCS. 2014.557 10.4230\/LIPIcs.FSTTCS.2014.557 Mary Southern and Kaustuv Chaudhuri. 2014. A Two-Level Logic Approach to Reasoning About Typed Specification Languages. In 34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014)(Leibniz International Proceedings in Informatics (LIPIcs), Vol.\u00a029), Venkatesh Raman and S.\u00a0P. Suresh (Eds.). Dagstuhl, Germany, 557\u2013569. https:\/\/doi.org\/10.4230\/LIPIcs.FSTTCS.2014.557"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.337.8"},{"key":"e_1_3_2_1_20_1","volume-title":"Int. Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP\u201906)","author":"Tiu Alwen","year":"2006","unstructured":"Alwen Tiu . 2006 . A Logic for Reasoning about Generic Judgments . In Int. Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP\u201906) (ENTCS, Vol.\u00a0173), A.\u00a0Momigliano and B.\u00a0Pientka (Eds.). 3\u201318. https:\/\/doi.org\/10.1016\/j.entcs. 2007.01.016 10.1016\/j.entcs.2007.01.016 Alwen Tiu. 2006. A Logic for Reasoning about Generic Judgments. In Int. Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP\u201906)(ENTCS, Vol.\u00a0173), A.\u00a0Momigliano and B.\u00a0Pientka (Eds.). 3\u201318. https:\/\/doi.org\/10.1016\/j.entcs.2007.01.016"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/2503887.2503893"}],"event":{"name":"PPDP 2022: 24th International Symposium on Principles and Practice of Declarative Programming","acronym":"PPDP 2022","location":"Tbilisi Georgia"},"container-title":["Proceedings of the 24th International Symposium on Principles and Practice of Declarative Programming"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3551357.3551377","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3551357.3551377","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3551357.3551377","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T19:00:24Z","timestamp":1750186824000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3551357.3551377"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,9,20]]},"references-count":21,"alternative-id":["10.1145\/3551357.3551377","10.1145\/3551357"],"URL":"https:\/\/doi.org\/10.1145\/3551357.3551377","relation":{},"subject":[],"published":{"date-parts":[[2022,9,20]]},"assertion":[{"value":"2022-09-20","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}