{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,2]],"date-time":"2026-10-02T12:49:13Z","timestamp":1790945353977,"version":"4.1.0"},"reference-count":117,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2019,1,2]],"date-time":"2019-01-02T00:00:00Z","timestamp":1546387200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["CCF-1619272, SHF-1814900, SHF-1817145"],"award-info":[{"award-number":["CCF-1619272, SHF-1814900, SHF-1817145"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000185","name":"Defense Advanced Research Projects Agency","doi-asserted-by":"publisher","award":["FA8750-16-2-0042"],"award-info":[{"award-number":["FA8750-16-2-0042"]}],"id":[{"id":"10.13039\/100000185","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2019,1,2]]},"abstract":"<jats:p>Live programming environments aim to provide programmers (and sometimes audiences) with continuous feedback about a program's dynamic behavior as it is being edited. The problem is that programming languages typically assign dynamic meaning only to programs that are complete, i.e. syntactically well-formed and free of type errors. Consequently, live feedback presented to the programmer exhibits temporal or perceptive gaps.<\/jats:p>\n          <jats:p>This paper confronts this \"gap problem\" from type-theoretic first principles by developing a dynamic semantics for incomplete functional programs, starting from the static semantics for incomplete functional programs developed in recent work on Hazelnut. We model incomplete functional programs as expressions with holes, with empty holes standing for missing expressions or types, and non-empty holes operating as membranes around static and dynamic type inconsistencies. Rather than aborting when evaluation encounters any of these holes as in some existing systems, evaluation proceeds around holes, tracking the closure around each hole instance as it flows through the remainder of the program. Editor services can use the information in these hole closures to help the programmer develop and confirm their mental model of the behavior of the complete portions of the program as they decide how to fill the remaining holes. Hole closures also enable a fill-and-resume operation that avoids the need to restart evaluation after edits that amount to hole filling. Formally, the semantics borrows machinery from both gradual type theory (which supplies the basis for handling unfilled type holes) and contextual modal type theory (which supplies a logical basis for hole closures), combining these and developing additional machinery necessary to continue evaluation past holes while maintaining type safety. We have mechanized the metatheory of the core calculus, called Hazelnut Live, using the Agda proof assistant.<\/jats:p>\n          <jats:p>We have also implemented these ideas into the Hazel programming environment. The implementation inserts holes automatically, following the Hazelnut edit action calculus, to guarantee that every editor state has some (possibly incomplete) type. Taken together with this paper's type safety property, the result is a proof-of-concept live programming environment where rich dynamic feedback is truly available without gaps, i.e. for every reachable editor state.<\/jats:p>","DOI":"10.1145\/3290327","type":"journal-article","created":{"date-parts":[[2019,1,4]],"date-time":"2019-01-04T13:33:51Z","timestamp":1546608831000},"page":"1-32","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":52,"title":["Live functional programming with typed holes"],"prefix":"10.1145","volume":"3","author":[{"given":"Cyrus","family":"Omar","sequence":"first","affiliation":[{"name":"University of Chicago, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Ian","family":"Voysey","sequence":"additional","affiliation":[{"name":"Carnegie Mellon University, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Ravi","family":"Chugh","sequence":"additional","affiliation":[{"name":"University of Chicago, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Matthew A.","family":"Hammer","sequence":"additional","affiliation":[{"name":"University of Colorado Boulder, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2019,1,2]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796800000186"},{"key":"e_1_2_2_2_1","volume-title":"Explicit Substitutions for Contextual Type Theory. In International Workshop on Logical Frameworks and Meta-languages: Theory and Practice (LFMTP).","author":"Abel Andreas","year":"2010"},{"key":"e_1_2_2_3_1","volume-title":"Research Topics in Functional Programming","author":"Abramsky Samson"},{"key":"e_1_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/2384592.2384595"},{"key":"e_1_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1137\/0201022"},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/2997364.2997374"},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1109\/VLHCC.2014.6883014"},{"key":"e_1_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2012.21"},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/11541868_4"},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/3182657"},{"key":"e_1_2_2_11_1","volume-title":"The Lambda Calculus. Studies in Logic","author":"Barendregt H.P."},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/1985793.1985864"},{"key":"e_1_2_2_13_1","volume-title":"Processes, Terms and Cycles: Steps on the Road to Infinity, Essays Dedicated to Jan Willem Klop, on the Occasion of His 60th Birthday (Lecture Notes in Computer Science)","author":"Blanc Tomasz"},{"key":"e_1_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/1863523.1863540"},{"key":"e_1_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1017\/S095679681300018X"},{"key":"e_1_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/2491956.2462170"},{"key":"e_1_2_2_17_1","volume-title":"IEEE Symposium on Visual Languages.","author":"Burnett Margaret M."},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535863"},{"key":"e_1_2_2_20_1","volume-title":"Systematic identification and communication of type errors. J. Funct. Program. 28","author":"Chen Sheng","year":"2018"},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/1040294.1040301"},{"key":"e_1_2_2_22_1","unstructured":"David Raymond Christiansen. 2013. Bidirectional Typing Rules: A Tutorial. http:\/\/davidchristiansen.dk\/tutorials\/bidirectional. pdf .  David Raymond Christiansen. 2013. Bidirectional Typing Rules: A Tutorial. http:\/\/davidchristiansen.dk\/tutorials\/bidirectional. pdf ."},{"key":"e_1_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/2908080.2908103"},{"key":"e_1_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837632"},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(91)90230-Y"},{"key":"e_1_2_2_26_1","volume-title":"Elm: Concurrent FRP for Functional GUIs. Senior thesis","author":"Czaplicki Evan","year":"2012"},{"key":"e_1_2_2_27_1","volume-title":"An Introduction to Elm. (2018). https:\/\/guide.elm-lang.org\/ . Retrieved","author":"Czaplicki Evan","year":"2018"},{"key":"e_1_2_2_28_1","volume-title":"International Workshop on Trends in Functional Programming in Education (TFPIE).","author":"D\u2019Alves Curtis","year":"2017"},{"key":"e_1_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/582153.582176"},{"key":"e_1_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/382780.382785"},{"key":"e_1_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.2002.3147"},{"key":"e_1_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158126"},{"key":"e_1_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/2500365.2500582"},{"key":"e_1_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(92)90014-7"},{"key":"e_1_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/2643135.2643153"},{"key":"e_1_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1080\/08993400802114508"},{"key":"e_1_2_2_37_1","volume-title":"Retrieved","author":"Developers Flutter","year":"2017"},{"key":"e_1_2_2_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837629"},{"key":"e_1_2_2_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/2500365.2500603"},{"key":"e_1_2_2_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676992"},{"key":"e_1_2_2_41_1","volume-title":"Open Proofs and Open Terms: A Basis for Interactive Logic. In International Workshop on Computer Science Logic (CSL).","author":"Geuvers Herman"},{"key":"e_1_2_2_42_1","volume-title":"Smalltalk-80: the language and its implementation","author":"Goldberg Adele"},{"key":"e_1_2_2_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/800229.806967"},{"key":"e_1_2_2_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/2445196.2445368"},{"key":"e_1_2_2_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/2594291.2594324"},{"key":"e_1_2_2_46_1","volume-title":"Practical Foundations for Programming Languages","author":"Harper Robert","edition":"2"},{"key":"e_1_2_2_47_1","volume-title":"Proof, Language and Interaction: Essays in Honour of Robin Milner","author":"Harper Robert"},{"key":"e_1_2_2_48_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-27705-4_22"},{"key":"e_1_2_2_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/2984511.2984575"},{"key":"e_1_2_2_50_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10990-011-9066-z"},{"key":"e_1_2_2_51_1","doi-asserted-by":"publisher","DOI":"10.1145\/1108970.1108971"},{"key":"e_1_2_2_52_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2013.10"},{"key":"e_1_2_2_53_1","doi-asserted-by":"publisher","DOI":"10.1145\/3110284"},{"key":"e_1_2_2_54_1","volume-title":"Retrieved","author":"Jones Mike","year":"2017"},{"key":"e_1_2_2_55_1","volume-title":"Partial evaluation and automatic program generation","author":"Jones Neil D."},{"key":"e_1_2_2_56_1","volume-title":"Coroutines and Networks of Parallel Processes. In IFIP Congress. 993\u2013998","author":"Kahn Gilles"},{"key":"e_1_2_2_57_1","doi-asserted-by":"publisher","DOI":"10.1145\/1640089.1640122"},{"key":"e_1_2_2_58_1","doi-asserted-by":"publisher","DOI":"10.1145\/360248.360252"},{"key":"e_1_2_2_59_1","doi-asserted-by":"publisher","DOI":"10.1145\/3240719.3241791"},{"key":"e_1_2_2_60_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009856"},{"key":"e_1_2_2_61_1","doi-asserted-by":"publisher","DOI":"10.1145\/1159876.1159887"},{"key":"e_1_2_2_62_1","doi-asserted-by":"publisher","DOI":"10.5555\/646837.708490"},{"key":"e_1_2_2_63_1","unstructured":"Eyal Lotem and Yair Chuchem. 2016. Project Lamdu. http:\/\/www.lamdu.org\/ . Accessed: 2016-04-08.  Eyal Lotem and Yair Chuchem. 2016. Project Lamdu. http:\/\/www.lamdu.org\/ . Accessed: 2016-04-08."},{"key":"e_1_2_2_64_1","volume-title":"The implementation of ALF: a proof editor","author":"Magnusson Lena"},{"key":"e_1_2_2_66_1","doi-asserted-by":"publisher","DOI":"10.1080\/08993400802114581"},{"key":"e_1_2_2_67_1","doi-asserted-by":"publisher","DOI":"10.1145\/1297027.1297073"},{"key":"e_1_2_2_68_1","doi-asserted-by":"publisher","DOI":"10.1145\/1352582.1352591"},{"key":"e_1_2_2_69_1","doi-asserted-by":"publisher","DOI":"10.1145\/3105726.3106178"},{"key":"e_1_2_2_71_1","doi-asserted-by":"publisher","DOI":"10.1145\/1481861.1481862"},{"key":"e_1_2_2_72_1","doi-asserted-by":"publisher","DOI":"10.1145\/360204.360207"},{"key":"e_1_2_2_73_1","volume-title":"Hammer","author":"Omar Cyrus","year":"2018"},{"key":"e_1_2_2_74_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009900"},{"key":"e_1_2_2_75_1","volume-title":"Jonathan Aldrich, and Matthew A. Hammer.","author":"Omar Cyrus","year":"2017"},{"key":"e_1_2_2_76_1","doi-asserted-by":"publisher","DOI":"10.1145\/2784731.2784765"},{"key":"e_1_2_2_77_1","doi-asserted-by":"publisher","DOI":"10.1145\/2364527.2364579"},{"key":"e_1_2_2_78_1","doi-asserted-by":"publisher","DOI":"10.1109\/MCSE.2007.53"},{"key":"e_1_2_2_79_1","volume-title":"Retrieved","author":"Jones Simon Peyton","year":"2014"},{"key":"e_1_2_2_80_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-12251-4_1"},{"key":"e_1_2_2_81_1","volume-title":"Inductive Beluga: Programming Proofs. In International Conference on Automated Deduction.","author":"Pientka Brigitte","year":"2015"},{"key":"e_1_2_2_82_1","doi-asserted-by":"publisher","DOI":"10.1145\/1389449.1389469"},{"key":"e_1_2_2_83_1","volume-title":"Types and Programming Languages","author":"Pierce Benjamin C."},{"key":"e_1_2_2_84_1","doi-asserted-by":"publisher","DOI":"10.1145\/345099.345100"},{"key":"e_1_2_2_85_1","volume-title":"A structural approach to operational semantics. J. Log. Algebr. Program. 60-61","author":"Plotkin Gordon D.","year":"2004"},{"key":"e_1_2_2_86_1","article-title":"Exploratory and Live, Programming and Coding - A Literature Study Comparing Perspectives on Liveness","volume":"3","author":"Rein Patrick","year":"2019","journal-title":"Programming Journal"},{"key":"e_1_2_2_87_1","doi-asserted-by":"publisher","DOI":"10.1145\/1592761.1592779"},{"key":"e_1_2_2_88_1","doi-asserted-by":"publisher","DOI":"10.1145\/3110258"},{"key":"e_1_2_2_89_1","doi-asserted-by":"publisher","DOI":"10.1145\/2228360.2228526"},{"key":"e_1_2_2_90_1","doi-asserted-by":"publisher","DOI":"10.1145\/2951913.2951915"},{"key":"e_1_2_2_91_1","volume-title":"Gradual Typing for Functional Languages. In Scheme and Functional Programming Workshop. http:\/\/scheme2006","author":"Jeremy"},{"key":"e_1_2_2_92_1","volume-title":"Gradual Typing for Objects. In European Conference on Object-Oriented Programming (ECOOP).","author":"Jeremy"},{"key":"e_1_2_2_93_1","unstructured":"Jeremy G. Siek Michael M. Vitousek Matteo Cimini and John Tang Boyland. 2015a. Refined Criteria for Gradual Typing. In Summit on Advances in Programming Languages (SNAPL).  Jeremy G. Siek Michael M. Vitousek Matteo Cimini and John Tang Boyland. 2015a. Refined Criteria for Gradual Typing. In Summit on Advances in Programming Languages (SNAPL)."},{"key":"e_1_2_2_94_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46669-8_18"},{"key":"e_1_2_2_95_1","doi-asserted-by":"publisher","DOI":"10.1145\/1706299.1706342"},{"key":"e_1_2_2_96_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-10672-9_3"},{"key":"e_1_2_2_97_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-012-0223-4"},{"key":"e_1_2_2_98_1","doi-asserted-by":"publisher","DOI":"10.1145\/1255450.1255455"},{"key":"e_1_2_2_99_1","series-title":"Automated Deduction \u2014 A Basis for Applications.","volume-title":"Foundations","author":"Strecker M."},{"key":"e_1_2_2_100_1","doi-asserted-by":"publisher","DOI":"10.1145\/3196321.3196364"},{"key":"e_1_2_2_101_1","volume-title":"Towards Practical Gradual Typing. In European Conference on Object-Oriented Programming (ECOOP).","author":"Takikawa Asumu","year":"2015"},{"key":"e_1_2_2_102_1","doi-asserted-by":"publisher","DOI":"10.1016\/S1045-926X(05)80012-6"},{"key":"e_1_2_2_103_1","doi-asserted-by":"publisher","DOI":"10.5555\/2662726.2662735"},{"key":"e_1_2_2_104_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796800001313"},{"key":"e_1_2_2_105_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-73595-3_4"},{"key":"e_1_2_2_106_1","unstructured":"B Victor. 2012. Inventing on principle Invited talk at the Canadian University Software Engineering Conference (CUSEC). http:\/\/worrydream.com\/#!\/InventingOnPrinciple  B Victor. 2012. Inventing on principle Invited talk at the Canadian University Software Engineering Conference (CUSEC). http:\/\/worrydream.com\/#!\/InventingOnPrinciple"},{"key":"e_1_2_2_107_1","doi-asserted-by":"publisher","DOI":"10.1145\/2384716.2384767"},{"key":"e_1_2_2_108_1","volume-title":"Towards User-Friendly Projectional Editors. In International Conference on Software Language Engineering (SLE).","author":"Voelter Markus","year":"2014"},{"key":"e_1_2_2_109_1","doi-asserted-by":"publisher","DOI":"10.1145\/2364527.2364554"},{"key":"e_1_2_2_110_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-00590-9_1"},{"key":"e_1_2_2_111_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796806006186"},{"key":"e_1_2_2_112_1","volume-title":"The Psychology of Computer Programming","author":"Weinberg Gerald M"},{"key":"e_1_2_2_113_1","doi-asserted-by":"publisher","DOI":"10.1145\/3173574.3173940"},{"key":"e_1_2_2_114_1","doi-asserted-by":"publisher","DOI":"10.1145\/2771839.2771860"},{"key":"e_1_2_2_115_1","volume-title":"Visualizing the Evaluation of Functional Programs for Debugging. In Symposium on Languages, Applications and Technologies (SLATE).","author":"Whitington John","year":"2017"},{"key":"e_1_2_2_116_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1994.1093"},{"key":"e_1_2_2_117_1","volume-title":"Consistent Subtyping for All. In European Symposium on Programming (ESOP).","author":"Xie Ningning"},{"key":"e_1_2_2_118_1","volume-title":"IEEE Symposium on Visual Languages and Human-Centric Computing (VL\/HCC).","author":"Yoon Y. S."},{"key":"e_1_2_2_119_1","doi-asserted-by":"publisher","DOI":"10.1145\/3121137"},{"key":"e_1_2_2_120_1","volume-title":"International Conference on Computer Science and Software Engineering (CASCON).","author":"Zhang John","year":"2018"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3290327","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3290327","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3290327","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T01:02:07Z","timestamp":1750208527000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3290327"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,1,2]]},"references-count":117,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2019,1,2]]}},"alternative-id":["10.1145\/3290327"],"URL":"https:\/\/doi.org\/10.1145\/3290327","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019,1,2]]},"assertion":[{"value":"2019-01-02","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}