{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,10]],"date-time":"2026-04-10T03:12:06Z","timestamp":1775790726586,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":34,"publisher":"ACM","license":[{"start":{"date-parts":[[2022,6,9]],"date-time":"2022-06-09T00:00:00Z","timestamp":1654732800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2022,6,9]]},"DOI":"10.1145\/3519939.3523707","type":"proceedings-article","created":{"date-parts":[[2022,6,2]],"date-time":"2022-06-02T21:05:05Z","timestamp":1654203905000},"page":"966-980","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":14,"title":["Computing correctly with inductive relations"],"prefix":"10.1145","author":[{"given":"Zoe","family":"Paraskevopoulou","sequence":"first","affiliation":[{"name":"Northeastern University, USA"}]},{"given":"Aaron","family":"Eline","sequence":"additional","affiliation":[{"name":"University of Maryland, USA"}]},{"given":"Leonidas","family":"Lampropoulos","sequence":"additional","affiliation":[{"name":"University of Maryland, USA"}]}],"member":"320","published-online":{"date-parts":[[2022,6,9]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/1411273.1411275"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03359-9_11"},{"key":"e_1_3_2_1_3_1","volume-title":"Executing Higher Order Logic. In International Workshop on Types for Proofs and Programs (TYPES) (Lecture Notes in Computer Science","volume":"40","author":"Berghofer Stefan","year":"2002","unstructured":"Stefan Berghofer and Tobias Nipkow . 2002 . Executing Higher Order Logic. In International Workshop on Types for Proofs and Programs (TYPES) (Lecture Notes in Computer Science , Vol. 2277). Springer, 24\u2013 40 . isbn:3-540-43287-6 http:\/\/www4.in.tum.de\/publ\/papers\/TYPES2000.pdf Stefan Berghofer and Tobias Nipkow. 2002. Executing Higher Order Logic. In International Workshop on Types for Proofs and Programs (TYPES) (Lecture Notes in Computer Science, Vol. 2277). Springer, 24\u201340. isbn:3-540-43287-6 http:\/\/www4.in.tum.de\/publ\/papers\/TYPES2000.pdf"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-07964-5_16"},{"key":"e_1_3_2_1_5_1","volume-title":"2nd International Conference on Certified Programs and Proofs (CPP) (Lecture Notes in Computer Science","volume":"108","author":"Bulwahn Lukas","year":"2012","unstructured":"Lukas Bulwahn . 2012 . The New Quickcheck for Isabelle - Random, Exhaustive and Symbolic Testing under One Roof . In 2nd International Conference on Certified Programs and Proofs (CPP) (Lecture Notes in Computer Science , Vol. 7679). Springer, 92\u2013 108 . https:\/\/www.irisa.fr\/celtique\/genet\/ACF\/BiblioIsabelle\/quickcheckNew.pdf Lukas Bulwahn. 2012. The New Quickcheck for Isabelle - Random, Exhaustive and Symbolic Testing under One Roof. In 2nd International Conference on Certified Programs and Proofs (CPP) (Lecture Notes in Computer Science, Vol. 7679). Springer, 92\u2013108. https:\/\/www.irisa.fr\/celtique\/genet\/ACF\/BiblioIsabelle\/quickcheckNew.pdf"},{"key":"e_1_3_2_1_6_1","volume-title":"Smart Testing of Functional Programs in Isabelle. In 18th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR) (Lecture Notes in Computer Science","volume":"167","author":"Bulwahn Lukas","year":"2012","unstructured":"Lukas Bulwahn . 2012 . Smart Testing of Functional Programs in Isabelle. In 18th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR) (Lecture Notes in Computer Science , Vol. 7180). Springer, 153\u2013 167 . isbn:978-3-642-28716-9 http:\/\/citeseerx.ist.psu.edu\/viewdoc\/download?doi=10.1.1.229.1307&rep=rep1&type=pdf Lukas Bulwahn. 2012. Smart Testing of Functional Programs in Isabelle. In 18th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR) (Lecture Notes in Computer Science, Vol. 7180). Springer, 153\u2013167. isbn:978-3-642-28716-9 http:\/\/citeseerx.ist.psu.edu\/viewdoc\/download?doi=10.1.1.229.1307&rep=rep1&type=pdf"},{"key":"e_1_3_2_1_7_1","volume-title":"Integrating Testing and Interactive Theorem Proving. In 10th International Workshop on the ACL2 Theorem Prover and its Applications (EPTCS","volume":"19","author":"Chamarthi Harsh Raju","year":"2011","unstructured":"Harsh Raju Chamarthi , Peter C. Dillinger , Matt Kaufmann , and Panagiotis Manolios . 2011 . Integrating Testing and Interactive Theorem Proving. In 10th International Workshop on the ACL2 Theorem Prover and its Applications (EPTCS , Vol. 70). 4\u2013 19 . arxiv:1105.4394 Harsh Raju Chamarthi, Peter C. Dillinger, Matt Kaufmann, and Panagiotis Manolios. 2011. Integrating Testing and Interactive Theorem Proving. In 10th International Workshop on the ACL2 Theorem Prover and its Applications (EPTCS, Vol. 70). 4\u201319. arxiv:1105.4394"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-07151-0_2"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/351240.351266"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.4501022"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-74591-4_7"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-31862-0_25"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46669-8_16"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/1806799.1806835"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-72019-3_10"},{"key":"e_1_3_2_1_16_1","volume-title":"Code Generation via Higher-Order Rewrite Systems","author":"Haftmann Florian","unstructured":"Florian Haftmann and Tobias Nipkow . 2010. Code Generation via Higher-Order Rewrite Systems . In Functional and Logic Programming, Matthias Blume, Naoki Kobayashi, and Germ\u00e1n Vidal (Eds.). Springer Berlin Heidelberg , Berlin, Heidelberg . 103\u2013117. isbn:978-3-642-12251-4 Florian Haftmann and Tobias Nipkow. 2010. Code Generation via Higher-Order Rewrite Systems. In Functional and Logic Programming, Matthias Blume, Naoki Kobayashi, and Germ\u00e1n Vidal (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg. 103\u2013117. isbn:978-3-642-12251-4"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/11737414_3"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/2500365.2500574"},{"key":"e_1_3_2_1_20_1","volume-title":"20th International Symposium on Trends in Functional Programming.","author":"Hughes John","year":"2019","unstructured":"John Hughes . 2019 . How to Specify It! . 20th International Symposium on Trends in Functional Programming. John Hughes. 2019. How to Specify It!. 20th International Symposium on Trends in Functional Programming."},{"key":"e_1_3_2_1_21_1","volume-title":"Randomized Testing in PLT Redex. In Workshop on Scheme and Functional Programming (SFP). http:\/\/www.eecs.northwestern.edu\/~robby\/pubs\/papers\/scheme2009-kf.pdf","author":"Klein Casey","year":"2009","unstructured":"Casey Klein and Robert Bruce Findler . 2009 . Randomized Testing in PLT Redex. In Workshop on Scheme and Functional Programming (SFP). http:\/\/www.eecs.northwestern.edu\/~robby\/pubs\/papers\/scheme2009-kf.pdf Casey Klein and Robert Bruce Findler. 2009. Randomized Testing in PLT Redex. In Workshop on Scheme and Functional Programming (SFP). http:\/\/www.eecs.northwestern.edu\/~robby\/pubs\/papers\/scheme2009-kf.pdf"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/2637647.2637655"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158133"},{"key":"e_1_3_2_1_25_1","volume-title":"Pierce","author":"Lampropoulos Leonidas","year":"2018","unstructured":"Leonidas Lampropoulos and Benjamin C . Pierce . 2018 . QuickCHick: Property- Based Testing In Coq. Electronic textbook. http:\/\/www.cis.upenn.edu\/~bcpierce\/sf Leonidas Lampropoulos and Benjamin C. Pierce. 2018. QuickCHick: Property-Based Testing In Coq. Electronic textbook. http:\/\/www.cis.upenn.edu\/~bcpierce\/sf"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796817000107"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/1481861.1481862"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/2034654.2034663"},{"key":"e_1_3_2_1_29_1","volume-title":"The Fifth International Workshop on Coq for Programming LanguagesCoqPL. https:\/\/www.p\u00e9drot.fr\/articles\/coqpl2019","author":"P\u00e9drot Pierre-Marie","year":"2019","unstructured":"Pierre-Marie P\u00e9drot . 2019 . Ltac2: Tactical Warfare . The Fifth International Workshop on Coq for Programming LanguagesCoqPL. https:\/\/www.p\u00e9drot.fr\/articles\/coqpl2019 .pdfpdf Pierre-Marie P\u00e9drot. 2019. Ltac2: Tactical Warfare. The Fifth International Workshop on Coq for Programming LanguagesCoqPL. https:\/\/www.p\u00e9drot.fr\/articles\/coqpl2019.pdfpdf"},{"key":"e_1_3_2_1_30_1","volume-title":"Chris Casinghino, Marco Gaboardi, Michael Greenberg, C\u01cet\u01celin Hri\u0163cu, Vilhelm Sj\u00f6berg, Andrew Tolmach, and Brent Yorgey.","author":"Pierce Benjamin C.","year":"2018","unstructured":"Benjamin C. Pierce , Arthur Azevedo de Amorim , Chris Casinghino, Marco Gaboardi, Michael Greenberg, C\u01cet\u01celin Hri\u0163cu, Vilhelm Sj\u00f6berg, Andrew Tolmach, and Brent Yorgey. 2018 . Programming Language Foundations. Electronic textbook, Version 5.5.. http:\/\/www.cis.upenn.edu\/~bcpierce\/sf Benjamin C. Pierce, Arthur Azevedo de Amorim, Chris Casinghino, Marco Gaboardi, Michael Greenberg, C\u01cet\u01celin Hri\u0163cu, Vilhelm Sj\u00f6berg, Andrew Tolmach, and Brent Yorgey. 2018. Programming Language Foundations. Electronic textbook, Version 5.5.. http:\/\/www.cis.upenn.edu\/~bcpierce\/sf"},{"key":"e_1_3_2_1_31_1","volume-title":"Chris Casinghino, Marco Gaboardi, Michael Greenberg, C\u01cet\u01celin Hri\u0163cu, Vilhelm Sj\u00f6berg, and Brent Yorgey.","author":"Pierce Benjamin C.","year":"2018","unstructured":"Benjamin C. Pierce , Arthur Azevedo de Amorim , Chris Casinghino, Marco Gaboardi, Michael Greenberg, C\u01cet\u01celin Hri\u0163cu, Vilhelm Sj\u00f6berg, and Brent Yorgey. 2018 . Logical Foundations. Electronic textbook, Version 5.5. http:\/\/www.cis.upenn.edu\/~bcpierce\/sf Benjamin C. Pierce, Arthur Azevedo de Amorim, Chris Casinghino, Marco Gaboardi, Michael Greenberg, C\u01cet\u01celin Hri\u0163cu, Vilhelm Sj\u00f6berg, and Brent Yorgey. 2018. Logical Foundations. Electronic textbook, Version 5.5. http:\/\/www.cis.upenn.edu\/~bcpierce\/sf"},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0054170"},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-71067-7_23"},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-35308-6_9"},{"key":"e_1_3_2_1_35_1","unstructured":"Niki Vazou. 2016. Liquid Haskell: Haskell as a Theorem Prover. Ph.D. Dissertation. University of California San Diego USA. http:\/\/www.escholarship.org\/uc\/item\/8dm057ws  Niki Vazou. 2016. Liquid Haskell: Haskell as a Theorem Prover. Ph.D. Dissertation. University of California San Diego USA. http:\/\/www.escholarship.org\/uc\/item\/8dm057ws"},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-11931-6_5"}],"event":{"name":"PLDI '22: 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation","location":"San Diego CA USA","acronym":"PLDI '22","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages"]},"container-title":["Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3519939.3523707","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3519939.3523707","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T18:10:30Z","timestamp":1750183830000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3519939.3523707"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,6,9]]},"references-count":34,"alternative-id":["10.1145\/3519939.3523707","10.1145\/3519939"],"URL":"https:\/\/doi.org\/10.1145\/3519939.3523707","relation":{},"subject":[],"published":{"date-parts":[[2022,6,9]]},"assertion":[{"value":"2022-06-09","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}