{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,27]],"date-time":"2026-02-27T03:46:44Z","timestamp":1772164004794,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":28,"publisher":"ACM","license":[{"start":{"date-parts":[[2015,1,14]],"date-time":"2015-01-14T00:00:00Z","timestamp":1421193600000},"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":["910500"],"award-info":[{"award-number":["910500"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["1116620"],"award-info":[{"award-number":["1116620"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["1319880"],"award-info":[{"award-number":["1319880"]}],"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":[[2015,1,14]]},"DOI":"10.1145\/2676726.2676974","type":"proceedings-article","created":{"date-parts":[[2014,12,19]],"date-time":"2014-12-19T08:51:05Z","timestamp":1418979065000},"page":"369-382","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":11,"title":["Programming up to Congruence"],"prefix":"10.1145","author":[{"given":"Vilhelm","family":"Sj\u00f6berg","sequence":"first","affiliation":[{"name":"University of Pennsylvania, Philadelphia, PA, USA"}]},{"given":"Stephanie","family":"Weirich","sequence":"additional","affiliation":[{"name":"University of Pennsylvania, Philadelphia, PA, USA"}]}],"member":"320","published-online":{"date-parts":[[2015,1,14]]},"reference":[{"key":"e_1_3_2_2_1_1","volume-title":"Japan","author":"Altenkirch T.","year":"2011","unstructured":"T. Altenkirch . The case of the smart case: How to implement conditional convertibility? Presentation at NII Shonan seminar 007 , Japan , Sept. 2011 . T. Altenkirch. The case of the smart case: How to implement conditional convertibility? Presentation at NII Shonan seminar 007, Japan, Sept. 2011."},{"key":"e_1_3_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/1292597.1292608"},{"key":"e_1_3_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/289423.289451"},{"key":"e_1_3_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1016\/B978-0-12-046371-8.50007-9"},{"key":"e_1_3_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.5555\/1792803.1792829"},{"key":"e_1_3_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.5555\/993954"},{"key":"e_1_3_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/1863543.1863560"},{"key":"e_1_3_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/1929529.1929536"},{"key":"e_1_3_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535883"},{"key":"e_1_3_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.5555\/1789277.1789283"},{"key":"e_1_3_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.5555\/1792734.1792766"},{"key":"e_1_3_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2004.06.068"},{"key":"e_1_3_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/322217.322228"},{"key":"e_1_3_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1988.5121"},{"key":"e_1_3_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/1411204.1411212"},{"key":"e_1_3_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.5555\/1939141.1939161"},{"key":"e_1_3_2_2_18_1","volume-title":"First-order unification by structural recursion","author":"McBride C.","year":"2001","unstructured":"C. McBride . First-order unification by structural recursion , 2001 . C. McBride. First-order unification by structural recursion, 2001."},{"key":"e_1_3_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/322186.322198"},{"key":"e_1_3_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2006.08.009"},{"key":"e_1_3_2_2_21_1","volume-title":"Proof Search in Type Theories (PSTT)","author":"Petcher A.","year":"2009","unstructured":"A. Petcher and A. Stump . Deciding Joinability Modulo Ground Equations in Operational Type Theory. In S. Lengrand and D. Miller, editors , Proof Search in Type Theories (PSTT) , 2009 . A. Petcher and A. Stump. Deciding Joinability Modulo Ground Equations in Operational Type Theory. In S. Lengrand and D. Miller, editors, Proof Search in Type Theories (PSTT), 2009."},{"key":"e_1_3_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/345099.345100"},{"key":"e_1_3_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796809990293"},{"key":"e_1_3_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/359545.359570"},{"key":"e_1_3_2_2_26_1","doi-asserted-by":"crossref","unstructured":"V.\n      Sj\u00f6berg C.\n      Casinghino K. Y.\n      Ahn N.\n      Collins H. D.\n     Eades III P.\n      Fu G.\n      Kimmell T.\n      Sheard A.\n      Stump and \n      S.\n      Weirich\n  . \n  Irrelevance heterogeneous equality and call-by-value dependent type systems\n  . In J. Chapman and P. B. Levy editors MSFP '12 volume \n  76\n   of \n  EPTCS pages \n  112\n  --\n  162\n  . \n  Open Publishing Association 2012\n  .  V. Sj\u00f6berg C. Casinghino K. Y. Ahn N. Collins H. D. Eades III P. Fu G. Kimmell T. Sheard A. Stump and S. Weirich. Irrelevance heterogeneous equality and call-by-value dependent type systems. In J. Chapman and P. B. Levy editors MSFP '12 volume 76 of EPTCS pages 112--162. Open Publishing Association 2012.","DOI":"10.4204\/EPTCS.76.9"},{"key":"e_1_3_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/2103656.2103690"},{"key":"e_1_3_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.5555\/1887459.1887501"},{"key":"e_1_3_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-32033-3_34"},{"key":"e_1_3_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/2034773.2034811"}],"event":{"name":"POPL '15: The 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages","location":"Mumbai India","acronym":"POPL '15","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages","SIGACT ACM Special Interest Group on Algorithms and Computation Theory"]},"container-title":["Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2676726.2676974","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2676726.2676974","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T02:13:03Z","timestamp":1750212783000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2676726.2676974"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015,1,14]]},"references-count":28,"alternative-id":["10.1145\/2676726.2676974","10.1145\/2676726"],"URL":"https:\/\/doi.org\/10.1145\/2676726.2676974","relation":{"is-identical-to":[{"id-type":"doi","id":"10.1145\/2775051.2676974","asserted-by":"object"}]},"subject":[],"published":{"date-parts":[[2015,1,14]]},"assertion":[{"value":"2015-01-14","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}