{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:12:28Z","timestamp":1750306348889,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":17,"publisher":"ACM","license":[{"start":{"date-parts":[[2016,6,23]],"date-time":"2016-06-23T00:00:00Z","timestamp":1466640000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/501100000038","name":"Natural Sciences and Engineering Research Council of Canada","doi-asserted-by":"publisher","award":["234341, 206263, 444462-2013"],"award-info":[{"award-number":["234341, 206263, 444462-2013"]}],"id":[{"id":"10.13039\/501100000038","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2016,6,23]]},"DOI":"10.1145\/2966268.2966269","type":"proceedings-article","created":{"date-parts":[[2016,9,9]],"date-time":"2016-09-09T14:28:57Z","timestamp":1473431337000},"page":"1-9","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Mechanizing Proofs about Mendler-style Recursion"],"prefix":"10.1145","author":[{"given":"Rohan","family":"Jacob-Rao","sequence":"first","affiliation":[{"name":"McGill University"}]},{"given":"Andrew","family":"Cave","sequence":"additional","affiliation":[{"name":"McGill University"}]},{"given":"Brigitte","family":"Pientka","sequence":"additional","affiliation":[{"name":"McGill University"}]}],"member":"320","published-online":{"date-parts":[[2016,6,23]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/96709.96712"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"crossref","unstructured":"A. Abel. Termination checking with types. RAIRO - Theoretical Informatics and Applications 38(4):277--319 3 2010.  A. Abel. Termination checking with types. RAIRO - Theoretical Informatics and Applications 38(4):277--319 3 2010.","DOI":"10.1051\/ita:2004015"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2004.10.017"},{"volume-title":"Princeton University","year":"2004","author":"Ahmed A.","key":"e_1_3_2_1_4_1"},{"key":"e_1_3_2_1_5_1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"13","DOI":"10.1007\/BFb0037095","volume-title":"International Conference on Typed Lambda Calculi and Applications (TLCA '93)","author":"Altenkirch T.","year":"1993"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/2071368.2071370"},{"issue":"2","key":"e_1_3_2_1_7_1","first-page":"1","article-title":"Abella: A system for reasoning about relational specifications","volume":"7","author":"Baelde D.","year":"2014","journal-title":"Journal of Formalized Reasoning"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-011-9219-0"},{"key":"e_1_3_2_1_9_1","first-page":"67","volume-title":"Proceedings of the First Workshop on Logical Frameworks","author":"Berardi S.","year":"1990"},{"volume-title":"Springer","year":"2004","author":"Bertot Y.","key":"e_1_3_2_1_10_1"},{"key":"e_1_3_2_1_11_1","first-page":"37181","volume-title":"Cambridge University Press","author":"Girard J.-Y.","year":"1989"},{"volume-title":"Cornell University","year":"1988","author":"Mendler N. P. F.","key":"e_1_3_2_1_12_1"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54833-8_8"},{"volume-title":"13th International Conference on Typed Lambda Calculi and Applications (TLCA'15), pages 273--287. Leibniz International Proceedings in Informatics (LIPIcs) of Schloss Dagstuhl","year":"2015","author":"Pientka B.","key":"e_1_3_2_1_15_1"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"crossref","unstructured":"B.\n       \n      Pientka\n     and \n      \n      \n      A.\n       \n      Cave\n      \n  \n  . \n  Inductive Beluga: Programming proofs (System description). In A. P. Felty and A. Middeldorp editors 25th International Conference on Automated Deduction (CADE-25) volume \n  9195\n   of \n  Lecture Notes in Computer Science pages \n  272\n  --\n  281\n  . \n  Springer 2015\n  .  B. Pientka and A. Cave. Inductive Beluga: Programming proofs (System description). In A. P. Felty and A. Middeldorp editors 25th International Conference on Automated Deduction (CADE-25) volume 9195 of Lecture Notes in Computer Science pages 272--281. Springer 2015.","DOI":"10.1007\/978-3-319-21401-6_18"},{"key":"e_1_3_2_1_17_1","series-title":"Lecture Notes in Computer Science (LNCS 9236)","doi-asserted-by":"crossref","first-page":"375","DOI":"10.1007\/978-3-319-22102-1_25","volume-title":"6th International Conference of Interactive Theorem Proving (ITP)","author":"Sieczkowski F.","year":"2015"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.2307\/2271658"}],"event":{"name":"LFMTP '16: Theory and Practice","acronym":"LFMTP '16","location":"Porto Portugal"},"container-title":["Proceedings of the Eleventh Workshop on Logical Frameworks and Meta-Languages: Theory and Practice"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2966268.2966269","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2966268.2966269","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:55:53Z","timestamp":1750222553000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2966268.2966269"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,6,23]]},"references-count":17,"alternative-id":["10.1145\/2966268.2966269","10.1145\/2966268"],"URL":"https:\/\/doi.org\/10.1145\/2966268.2966269","relation":{},"subject":[],"published":{"date-parts":[[2016,6,23]]},"assertion":[{"value":"2016-06-23","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}