{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T11:26:39Z","timestamp":1770290799822,"version":"3.49.0"},"reference-count":77,"publisher":"Association for Computing Machinery (ACM)","issue":"1","license":[{"start":{"date-parts":[[2014,3,1]],"date-time":"2014-03-01T00:00:00Z","timestamp":1393632000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/100000143","name":"Division of Computing and Communication Foundations","doi-asserted-by":"publisher","award":["CCF-0917092, CCF-1219165"],"award-info":[{"award-number":["CCF-0917092, CCF-1219165"]}],"id":[{"id":"10.13039\/100000143","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000181","name":"Air Force Office of Scientific Research","doi-asserted-by":"publisher","award":["FA9550-09-1-0229"],"award-info":[{"award-number":["FA9550-09-1-0229"]}],"id":[{"id":"10.13039\/100000181","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Program. Lang. Syst."],"published-print":{"date-parts":[[2014,3]]},"abstract":"<jats:p>\n            Through the use of conditional compilation and related tools, many software projects can be used to generate a huge number of related programs. The problem of typing such variational software is difficult. The brute-force strategy of generating all variants and typing each one individually is: (1) usually infeasible for efficiency reasons and (2) produces results that do not map well to the underlying variational program. Recent research has focused mainly on efficiency and addressed only the problem of type checking. In this work we tackle the more general problem of variational type inference and introduce variational types to represent the result of typing a variational program. We introduce the variational lambda calculus (VLC) as a formal foundation for research on typing variational programs. We define a type system for VLC in which VLC expressions are mapped to correspondingly variational types. We show that the type system is correct by proving that the typing of expressions is preserved over the process of variation elimination, which eventually results in a plain lambda calculus expression and its corresponding type. We identify a set of equivalence rules for variational types and prove that the type unification problem modulo these equivalence rules is unitary and decidable; we also present a sound and complete unification algorithm. Based on the unification algorithm, the variational type inference algorithm is an extension of algorithm\n            <jats:italic>W<\/jats:italic>\n            . We show that it is sound and complete and computes principal types. We also consider the extension of VLC with sum types, a necessary feature for supporting variational data types, and demonstrate that the previous theoretical results also hold under this extension. Finally, we characterize the complexity of variational type inference and demonstrate the efficiency gains over the brute-force strategy.\n          <\/jats:p>","DOI":"10.1145\/2518190","type":"journal-article","created":{"date-parts":[[2014,3,24]],"date-time":"2014-03-24T13:45:50Z","timestamp":1395668750000},"page":"1-54","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":36,"title":["Extending Type Inference to Variational Programs"],"prefix":"10.1145","volume":"36","author":[{"given":"Sheng","family":"Chen","sequence":"first","affiliation":[{"name":"Oregon State University"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Martin","family":"Erwig","sequence":"additional","affiliation":[{"name":"Oregon State University"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Eric","family":"Walkingshaw","sequence":"additional","affiliation":[{"name":"Oregon State University"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2014,3]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.5555\/1044941"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-004-2279-7"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/1745312.1745316"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.5381\/jot.2009.8.5.c5"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/1449913.1449931"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10515-010-0066-8"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.5555\/2486788.2486852"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.5555\/288771"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.5555\/827253.827741"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","unstructured":"Baader F. and Nipkow T. 1998. Term Rewriting and All That. Cambridge University Press.","DOI":"10.5555\/280474"},{"key":"e_1_2_1_11_1","doi-asserted-by":"crossref","unstructured":"Baader F. and Snyder W. 2001. Unification theory. In Handbook of Automated Reasoning A. Robinson and A. Voronkov Eds. North Holland 445--532.","DOI":"10.1016\/B978-044450813-3\/50010-2"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/964001.964007"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2004.23"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/2162049.2162052"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/97945.97982"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1109\/SPLC.2008.28"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535863"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/2364527.2364535"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/1806799.1806850"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/1985793.1985838"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.5555\/2337223.2337302"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.5555\/345203"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/582153.582176"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/349299.349309"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/1509837.1509846"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/1595696.1595733"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/2048066.2048113"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1305\/ndjfl\/1039724889"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/2162049.2162063"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/1111037.1111064"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/322217.322228"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/383845.383853"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/2063239.2063245"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/1173706.1173748"},{"key":"e_1_2_1_35_1","volume-title":"Reference: Racket. Tech. rep. PLT-TR-2010-1","author":"Flatt M.","year":"2010","unstructured":"Flatt, M. and PLT. 2010. Reference: Racket. Tech. rep. PLT-TR-2010-1, PLT Inc. http:\/\/racket-lang.org\/tr1\/."},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/1244381.1244400"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/1621607.1621613"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/2254064.2254103"},{"key":"e_1_2_1_40_1","unstructured":"GNU Project. 2009. The C preprocessor. Free software foundation. http:\/\/gcc.gnu.org\/onlinedocs\/cpp\/."},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-010-0101-1"},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/1167473.1167499"},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/1375581.1375592"},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/1890028.1890029"},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1007\/11561347_21"},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/1218563.1218584"},{"key":"e_1_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/1133981.1134014"},{"key":"e_1_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/1328438.1328475"},{"key":"e_1_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/1159842.1159848"},{"key":"e_1_2_1_50_1","doi-asserted-by":"crossref","unstructured":"Kang K. C. Cohen S. G. Hess J. A. Novak W. E. and Peterson A. S. 1990. Feature-oriented domain analysis (FODA) feasibility study. Tech. rep. CMU\/SEI-90-TR-21 Software Engineering Institute Carnegie Mellon University.","DOI":"10.21236\/ADA235785"},{"key":"e_1_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1145\/1368088.1368131"},{"key":"e_1_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1145\/2048066.2048128"},{"key":"e_1_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.1145\/2211616.2211617"},{"key":"e_1_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.1145\/2384616.2384673"},{"key":"e_1_2_1_55_1","doi-asserted-by":"publisher","DOI":"10.1145\/1868688.1868693"},{"key":"e_1_2_1_56_1","doi-asserted-by":"publisher","DOI":"10.1145\/1449913.1449919"},{"key":"e_1_2_1_57_1","unstructured":"Liebig J. von Rhein A. K\u00e4stner C. Apel S. D\u00f6rre J. and Lengauer C. 2012. Large-scale variability-aware type checking and dataflow analysis. Tech. rep. MIP-1212 Department of Informatics and Mathematics University of Passau. http:\/\/www.infosun.fim.uni-passau.de\/publications\/docs\/TR_LRKADL12.pdf."},{"key":"e_1_2_1_58_1","doi-asserted-by":"publisher","DOI":"10.1145\/643603.643613"},{"key":"e_1_2_1_59_1","doi-asserted-by":"publisher","DOI":"10.1145\/1041685.1029915"},{"key":"e_1_2_1_60_1","doi-asserted-by":"publisher","DOI":"10.1145\/1868294.1868319"},{"key":"e_1_2_1_61_1","doi-asserted-by":"publisher","DOI":"10.1145\/322186.322198"},{"key":"e_1_2_1_63_1","doi-asserted-by":"publisher","DOI":"10.1002\/(SICI)1096-9942(199901\/03)5:1%3C35::AID-TAPO4%3E3.0.CO;2-4"},{"key":"e_1_2_1_64_1","doi-asserted-by":"publisher","DOI":"10.5555\/645891.671440"},{"key":"e_1_2_1_65_1","doi-asserted-by":"publisher","DOI":"10.5555\/509043"},{"key":"e_1_2_1_66_1","doi-asserted-by":"publisher","DOI":"10.5555\/1095605"},{"key":"e_1_2_1_67_1","unstructured":"Reis G. D. and Stroustrup B. 2005. A formalism for C++. Tech. rep. ISO\/IEC SC22\/JTC1\/WG21. http:\/\/www.open-std.org\/jtc1\/SC22\/WG21\/docs\/papers\/2005\/n1885.pdf."},{"key":"e_1_2_1_68_1","doi-asserted-by":"publisher","DOI":"10.1145\/321250.321253"},{"key":"e_1_2_1_69_1","doi-asserted-by":"publisher","DOI":"10.1145\/636517.636528"},{"key":"e_1_2_1_70_1","doi-asserted-by":"publisher","DOI":"10.1145\/268946.268970"},{"key":"e_1_2_1_71_1","doi-asserted-by":"publisher","DOI":"10.1007\/11785477_19"},{"key":"e_1_2_1_72_1","doi-asserted-by":"publisher","DOI":"10.1145\/237721.237727"},{"key":"e_1_2_1_73_1","doi-asserted-by":"publisher","DOI":"10.5555\/193198"},{"key":"e_1_2_1_74_1","doi-asserted-by":"publisher","DOI":"10.5555\/646190.683564"},{"key":"e_1_2_1_75_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796807006569"},{"key":"e_1_2_1_76_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(00)00053-0"},{"key":"e_1_2_1_77_1","doi-asserted-by":"publisher","DOI":"10.1145\/1289971.1289989"},{"key":"e_1_2_1_78_1","doi-asserted-by":"publisher","DOI":"10.1145\/1167473.1167477"},{"key":"e_1_2_1_79_1","doi-asserted-by":"publisher","DOI":"10.1145\/292540.292560"}],"container-title":["ACM Transactions on Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2518190","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2518190","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2518190","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T20:14:13Z","timestamp":1750277653000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2518190"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,3]]},"references-count":77,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2014,3]]}},"alternative-id":["10.1145\/2518190"],"URL":"https:\/\/doi.org\/10.1145\/2518190","relation":{},"ISSN":["0164-0925","1558-4593"],"issn-type":[{"value":"0164-0925","type":"print"},{"value":"1558-4593","type":"electronic"}],"subject":[],"published":{"date-parts":[[2014,3]]},"assertion":[{"value":"2012-08-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2013-04-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2014-03-01","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}