{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:30:33Z","timestamp":1750221033376,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":36,"publisher":"ACM","license":[{"start":{"date-parts":[[2018,9,27]],"date-time":"2018-09-27T00:00:00Z","timestamp":1538006400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2018,9,27]]},"DOI":"10.1145\/3240719.3241791","type":"proceedings-article","created":{"date-parts":[[2018,9,18]],"date-time":"2018-09-18T12:11:39Z","timestamp":1537272699000},"page":"38-50","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":2,"title":["Extensible type-directed editing"],"prefix":"10.1145","author":[{"given":"Joomy","family":"Korkut","sequence":"first","affiliation":[{"name":"Wesleyan University, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"David Thrane","family":"Christiansen","sequence":"additional","affiliation":[{"name":"Galois, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2018,9,27]]},"reference":[{"volume-title":"Changelog for Agda-2.5.1","key":"e_1_3_2_1_1_1","unstructured":"2016. Changelog for Agda-2.5.1 . http:\/\/hackage.haskell.org\/package\/ Agda-2.5.1\/changelog . (16 April 2016). Accessed: 2018-05-19. 2016. Changelog for Agda-2.5.1. http:\/\/hackage.haskell.org\/package\/ Agda-2.5.1\/changelog . (16 April 2016). Accessed: 2018-05-19."},{"volume-title":"Generic Programming","author":"Altenkirch Thorsten","key":"e_1_3_2_1_2_1","unstructured":"Thorsten Altenkirch and Conor McBride . 2003. Generic programming within dependently typed programming . In Generic Programming . Springer , 1\u201320. Thorsten Altenkirch and Conor McBride. 2003. Generic programming within dependently typed programming. In Generic Programming. Springer, 1\u201320."},{"key":"e_1_3_2_1_3_1","volume-title":"The Fourth International Workshop on Coq for Programming Languages .","author":"Anand Abhishek","year":"2018","unstructured":"Abhishek Anand , Simon Boulier , Cyril Cohen , Matthieu Sozeau , and Nicolas Tabareau . 2018 . Typed Template Coq\u2013Certified MetaProgramming in Coq . In The Fourth International Workshop on Coq for Programming Languages . Abhishek Anand, Simon Boulier, Cyril Cohen, Matthieu Sozeau, and Nicolas Tabareau. 2018. Typed Template Coq\u2013Certified MetaProgramming in Coq. In The Fourth International Workshop on Coq for Programming Languages ."},{"key":"e_1_3_2_1_4_1","unstructured":"Lennart Augustsson. 2005. Announcing Djinn. http:\/\/permalink. gmane.org\/gmane.comp.lang.haskell.general\/12747 . (2005). Accessed: 2017-10-04.  Lennart Augustsson. 2005. Announcing Djinn. http:\/\/permalink. gmane.org\/gmane.comp.lang.haskell.general\/12747 . (2005). Accessed: 2017-10-04."},{"key":"e_1_3_2_1_6_1","unstructured":"William J Bowman. 2016. Growing a Proof Assistant. Higher-Order Programming with Effects .  William J Bowman. 2016. Growing a Proof Assistant. Higher-Order Programming with Effects ."},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1017\/S095679681300018X"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/2951913.2951932"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/2746325.2746326"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796818000011"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-21401-6_26"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.2307\/2275431"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/3110278"},{"key":"e_1_3_2_1_15_1","volume-title":"LIPIcs-Leibniz International Proceedings in Informatics","volume":"32","author":"Felleisen Matthias","year":"2015","unstructured":"Matthias Felleisen , Robert Bruce Findler , Matthew Flatt , Shriram Krishnamurthi , Eli Barzilay , Jay McCarthy , and Sam Tobin-Hochstadt . 2015 . The Racket manifesto . In LIPIcs-Leibniz International Proceedings in Informatics , Vol. 32 . Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik. Matthias Felleisen, Robert Bruce Findler, Matthew Flatt, Shriram Krishnamurthi, Eli Barzilay, Jay McCarthy, and Sam Tobin-Hochstadt. 2015. The Racket manifesto. In LIPIcs-Leibniz International Proceedings in Informatics , Vol. 32. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik."},{"key":"e_1_3_2_1_16_1","volume-title":"Robert Bruce Findler, and Matthias Felleisen","author":"Feltey Daniel","year":"2016","unstructured":"Daniel Feltey , Spencer P Florence , Tim Knutson , Vincent St-Amour , Ryan Culpepper , Matthew Flatt , Robert Bruce Findler, and Matthias Felleisen . 2016 . Languages the Racket Way. Language Workbench Challenge . Daniel Feltey, Spencer P Florence, Tim Knutson, Vincent St-Amour, Ryan Culpepper, Matthew Flatt, Robert Bruce Findler, and Matthias Felleisen. 2016. Languages the Racket Way. Language Workbench Challenge ."},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/317636.317793"},{"key":"e_1_3_2_1_18_1","volume-title":"Friedman and David Thrane Christiansen","author":"Daniel","year":"2018","unstructured":"Daniel P. Friedman and David Thrane Christiansen . 2018 . The Little Typer . MIT Press , Cambridge, MA, USA. Daniel P. Friedman and David Thrane Christiansen. 2018. The Little Typer . MIT Press, Cambridge, MA, USA."},{"volume-title":"Smalltalk-80: The Interactive Programming Environment","author":"Goldberg Adele","key":"e_1_3_2_1_19_1","unstructured":"Adele Goldberg . 1984. Smalltalk-80: The Interactive Programming Environment . Addison Wesley . Adele Goldberg. 1984. Smalltalk-80: The Interactive Programming Environment . Addison Wesley."},{"key":"e_1_3_2_1_20_1","volume-title":"The proof editor","author":"Hallgren Thomas","year":"1998","unstructured":"Thomas Hallgren . 1998. The proof editor Alfa . http:\/\/www.cse. chalmers.se\/hallgren\/Alfa . ( 1998 ). Thomas Hallgren. 1998. The proof editor Alfa. http:\/\/www.cse. chalmers.se\/hallgren\/Alfa . (1998)."},{"key":"e_1_3_2_1_21_1","unstructured":"Robert Harper. 1997. Notes on Regular Expression Simplification. https: \/\/www.cs.cmu.edu\/ \u223c fp\/courses\/97-212\/handouts\/regsimp.pdf . (1997). Accessed: 2017-06-06.  Robert Harper. 1997. Notes on Regular Expression Simplification. https: \/\/www.cs.cmu.edu\/ \u223c fp\/courses\/97-212\/handouts\/regsimp.pdf . (1997). Accessed: 2017-06-06."},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796805005769"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/242224.242477"},{"key":"e_1_3_2_1_24_1","volume-title":"Auto in Agda. In International Conference on Mathematics of Program Construction . Springer, 276\u2013301","author":"Kokke Wen","year":"2015","unstructured":"Wen Kokke and Wouter Swierstra . 2015 . Auto in Agda. In International Conference on Mathematics of Program Construction . Springer, 276\u2013301 . Wen Kokke and Wouter Swierstra. 2015. Auto in Agda. In International Conference on Mathematics of Program Construction . Springer, 276\u2013301."},{"volume-title":"Edit-Time Tactics in Idris. Master\u2019s thesis","author":"Korkut Joomy","key":"e_1_3_2_1_25_1","unstructured":"Joomy Korkut . 2018. Edit-Time Tactics in Idris. Master\u2019s thesis . Wesleyan University , Middletown, CT, USA . Joomy Korkut. 2018. Edit-Time Tactics in Idris. Master\u2019s thesis. Wesleyan University, Middletown, CT, USA."},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/11617990_10"},{"volume-title":"The implementation of ALF - a proof editor","author":"Magnusson Lena","key":"e_1_3_2_1_27_1","unstructured":"Lena Magnusson . 1994. The implementation of ALF - a proof editor based on Martin-L\u00a8of\u2019s monomorhic type theory with explicit substitution . Ph.D. Dissertation. Chalmers Tekniska H\u00a8ogskolan . Lena Magnusson. 1994. The implementation of ALF - a proof editor based on Martin-L\u00a8of\u2019s monomorhic type theory with explicit substitution . Ph.D. Dissertation. Chalmers Tekniska H\u00a8ogskolan."},{"key":"e_1_3_2_1_28_1","volume-title":"International Workshop on Types for Proofs and Programs . Springer, 213\u2013237","author":"Magnusson Lena","year":"1993","unstructured":"Lena Magnusson and Bengt Nordstr\u00a8om . 1993 . The ALF proof editor and its proof engine . In International Workshop on Types for Proofs and Programs . Springer, 213\u2013237 . Lena Magnusson and Bengt Nordstr\u00a8om. 1993. The ALF proof editor and its proof engine. In International Workshop on Types for Proofs and Programs . Springer, 213\u2013237."},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796803004829"},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796807006326"},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/367177.367199"},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009900"},{"key":"e_1_3_2_1_35_1","volume-title":"Jonathan Aldrich, and Matthew A. Hammer.","author":"Omar Cyrus","year":"2017","unstructured":"Cyrus Omar , Ian Voysey , Michael Hilton , Joshua Sunshine , Claire Le Goues , Jonathan Aldrich, and Matthew A. Hammer. 2017 . Toward Semantic Foundations for Program Editors. In Summit on Advances in Programming Languages (SNAPL 2017) . Cyrus Omar, Ian Voysey, Michael Hilton, Joshua Sunshine, Claire Le Goues, Jonathan Aldrich, and Matthew A. Hammer. 2017. Toward Semantic Foundations for Program Editors. In Summit on Advances in Programming Languages (SNAPL 2017) ."},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0378-4754(97)00086-4"},{"key":"e_1_3_2_1_37_1","volume-title":"Informal Proceedings of First Workshop on Logical Frameworks","volume":"4","author":"Pollack Robert","year":"1990","unstructured":"Robert Pollack . 1990 . Implicit syntax . In Informal Proceedings of First Workshop on Logical Frameworks , Antibes , Vol. 4 . Robert Pollack. 1990. Implicit syntax. In Informal Proceedings of First Workshop on Logical Frameworks, Antibes , Vol. 4."},{"key":"e_1_3_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/125826.125848"},{"key":"e_1_3_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/581690.581691"},{"key":"e_1_3_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/154766.155373"}],"event":{"name":"ICFP '18: 23nd ACM SIGPLAN International Conference on Functional Programming","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages"],"location":"St. Louis MO USA","acronym":"ICFP '18"},"container-title":["Proceedings of the 3rd ACM SIGPLAN International Workshop on Type-Driven Development"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3240719.3241791","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3240719.3241791","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T00:43:33Z","timestamp":1750207413000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3240719.3241791"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,9,27]]},"references-count":36,"alternative-id":["10.1145\/3240719.3241791","10.1145\/3240719"],"URL":"https:\/\/doi.org\/10.1145\/3240719.3241791","relation":{},"subject":[],"published":{"date-parts":[[2018,9,27]]},"assertion":[{"value":"2018-09-27","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}