{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,11]],"date-time":"2026-04-11T00:49:23Z","timestamp":1775868563840,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":26,"publisher":"ACM","license":[{"start":{"date-parts":[[2016,1,11]],"date-time":"2016-01-11T00:00:00Z","timestamp":1452470400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"JSPS (Japan Society for Promotion of Science)","award":["Grant-in-Aid for Scientific Research (A) No. 25240009"],"award-info":[{"award-number":["Grant-in-Aid for Scientific Research (A) No. 25240009"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2016,1,11]]},"DOI":"10.1145\/2847538.2847544","type":"proceedings-article","created":{"date-parts":[[2016,1,7]],"date-time":"2016-01-07T14:05:00Z","timestamp":1452175500000},"page":"61-72","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":49,"title":["BiGUL: a formally verified core language for putback-based bidirectional programming"],"prefix":"10.1145","author":[{"given":"Hsiang-Shang","family":"Ko","sequence":"first","affiliation":[{"name":"National Institute of Informatics, Japan"}]},{"given":"Tao","family":"Zan","sequence":"additional","affiliation":[{"name":"Sokendai, Japan \/ National Institute of Informatics, Japan"}]},{"given":"Zhenjiang","family":"Hu","sequence":"additional","affiliation":[{"name":"Sokendai, Japan \/ National Institute of Informatics, Japan"}]}],"member":"320","published-online":{"date-parts":[[2016,1,11]]},"reference":[{"key":"e_1_3_2_2_1_1","doi-asserted-by":"crossref","unstructured":"T. Altenkirch and C. McBride. Generic programming within dependently typed programming. In IFIP TC2\/WG2.1 Working Conference on Generic Programming pages 1\u201320. Kluwer B.V. 2003.   T. Altenkirch and C. McBride. Generic programming within dependently typed programming. In IFIP TC2\/WG2.1 Working Conference on Generic Programming pages 1\u201320. Kluwer B.V. 2003.","DOI":"10.1007\/978-0-387-35672-3_1"},{"key":"e_1_3_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/1863543.1863572"},{"key":"e_1_3_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/1142351.1142399"},{"key":"e_1_3_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/1411204.1411209"},{"key":"e_1_3_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02408-5_19"},{"key":"e_1_3_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/1111037.1111056"},{"key":"e_1_3_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/1232420.1232424"},{"key":"e_1_3_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/1411204.1411257"},{"key":"e_1_3_2_2_10_1","series-title":"Lecture Notes in Computer Science","first-page":"71","volume-title":"Spring School on Datatype-Generic Programming","author":"Gibbons J.","unstructured":"J. Gibbons . Datatype-generic programming . In Spring School on Datatype-Generic Programming , volume 4719 of Lecture Notes in Computer Science , pages 1\u2013 71 . Springer-Verlag, 2007. J. Gibbons. Datatype-generic programming. In Spring School on Datatype-Generic Programming, volume 4719 of Lecture Notes in Computer Science, pages 1\u201371. Springer-Verlag, 2007."},{"key":"e_1_3_2_2_11_1","series-title":"Lecture Notes in Computer Science","first-page":"28","volume-title":"Central European Functional Programming School","author":"Gibbons J.","unstructured":"J. Gibbons . Functional programming for domain-specific languages. In Central European Functional Programming School , volume 8606 of Lecture Notes in Computer Science , pages 1\u2013 28 . Springer-Verlag, 2015. J. Gibbons. Functional programming for domain-specific languages. In Central European Functional Programming School, volume 8606 of Lecture Notes in Computer Science, pages 1\u201328. Springer-Verlag, 2015."},{"key":"e_1_3_2_2_12_1","first-page":"81","volume-title":"International Workshop on Bidirectional Transformations","author":"Grohne H.","unstructured":"H. Grohne , A. L\u00f6h , and J. Voigtl\u00e4nder . Formalizing semantic bidirectionalization with dependent types . In International Workshop on Bidirectional Transformations , pages 75\u2013 81 . CEUR-WS, 2014. H. Grohne, A. L\u00f6h, and J. Voigtl\u00e4nder. Formalizing semantic bidirectionalization with dependent types. In International Workshop on Bidirectional Transformations, pages 75\u201381. CEUR-WS, 2014."},{"key":"e_1_3_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/1863543.1863573"},{"key":"e_1_3_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/1926385.1926428"},{"key":"e_1_3_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/2103656.2103715"},{"key":"e_1_3_2_2_16_1","first-page":"15","volume-title":"International Symposium on Formal Methods","volume":"8442","author":"Hu Z.","unstructured":"Z. Hu , H. Pacheco , and S. Fischer . Validity checking of putback transformations in bidirectional programming . In International Symposium on Formal Methods , volume 8442 , pages 1\u2013 15 . Springer-Verlag, 2014. Z. Hu, H. Pacheco, and S. Fischer. Validity checking of putback transformations in bidirectional programming. In International Symposium on Formal Methods, volume 8442, pages 1\u201315. Springer-Verlag, 2014."},{"key":"e_1_3_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/2503778.2503786"},{"key":"e_1_3_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/1291151.1291162"},{"key":"e_1_3_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(91)90052-4"},{"key":"e_1_3_2_2_21_1","series-title":"Lecture Notes in Computer Science","first-page":"266","volume-title":"Advanced Functional Programming","author":"Norell U.","unstructured":"U. Norell . Dependently typed programming in Agda . In Advanced Functional Programming , volume 5832 of Lecture Notes in Computer Science , pages 230\u2013 266 . Springer-Verlag, 2009. U. Norell. Dependently typed programming in Agda. In Advanced Functional Programming, volume 5832 of Lecture Notes in Computer Science, pages 230\u2013266. Springer-Verlag, 2009."},{"key":"e_1_3_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/2500365.2500610"},{"key":"e_1_3_2_2_23_1","series-title":"Lecture Notes in Computer Science","first-page":"352","volume-title":"Mathematics of Program Construction","author":"Pacheco H.","unstructured":"H. Pacheco and A. Cunha . Generic point-free lenses . In Mathematics of Program Construction , volume 6120 of Lecture Notes in Computer Science , pages 331\u2013 352 . Springer-Verlag, 2010. H. Pacheco and A. Cunha. Generic point-free lenses. In Mathematics of Program Construction, volume 6120 of Lecture Notes in Computer Science, pages 331\u2013352. Springer-Verlag, 2010."},{"key":"e_1_3_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/2543728.2543737"},{"key":"e_1_3_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/2643135.2643141"},{"key":"e_1_3_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/1480881.1480904"},{"key":"e_1_3_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/143165.143169"},{"key":"e_1_3_2_2_28_1","first-page":"50","volume-title":"International Workshop on Bidirectional Transformations","author":"Zhu Z.","unstructured":"Z. Zhu , H.-S. Ko , P. Martins , J. Saraiva , and Z. Hu . BiYacc: roll your parser and reflective printer into one . In International Workshop on Bidirectional Transformations , pages 43\u2013 50 . CEUR-WS, 2015. Z. Zhu, H.-S. Ko, P. Martins, J. Saraiva, and Z. Hu. BiYacc: roll your parser and reflective printer into one. In International Workshop on Bidirectional Transformations, pages 43\u201350. CEUR-WS, 2015."}],"event":{"name":"POPL '16: The 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages","location":"St. Petersburg FL USA","acronym":"POPL '16","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages","SIGACT ACM Special Interest Group on Algorithms and Computation Theory"]},"container-title":["Proceedings of the 2016 ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2847538.2847544","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2847538.2847544","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T05:43:27Z","timestamp":1750225407000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2847538.2847544"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,1,11]]},"references-count":26,"alternative-id":["10.1145\/2847538.2847544","10.1145\/2847538"],"URL":"https:\/\/doi.org\/10.1145\/2847538.2847544","relation":{},"subject":[],"published":{"date-parts":[[2016,1,11]]},"assertion":[{"value":"2016-01-11","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}