{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T08:04:31Z","timestamp":1743062671830,"version":"3.40.3"},"publisher-location":"Cham","reference-count":45,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031745577"},{"type":"electronic","value":"9783031745584"}],"license":[{"start":{"date-parts":[[2025,1,1]],"date-time":"2025-01-01T00:00:00Z","timestamp":1735689600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2025,1,1]],"date-time":"2025-01-01T00:00:00Z","timestamp":1735689600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2025]]},"DOI":"10.1007\/978-3-031-74558-4_1","type":"book-chapter","created":{"date-parts":[[2025,1,9]],"date-time":"2025-01-09T04:35:02Z","timestamp":1736397302000},"page":"1-21","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Structural Refactorings for\u00a0Exploring Dependently Typed Programming"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-1236-7160","authenticated-orcid":false,"given":"Adam D.","family":"Barwell","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6030-2885","authenticated-orcid":false,"given":"Christopher","family":"Brown","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-2428-6130","authenticated-orcid":false,"given":"Mun See","family":"Chang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0009-0001-0198-2750","authenticated-orcid":false,"given":"Constantine","family":"Theocharis","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2350-301X","authenticated-orcid":false,"given":"Simon","family":"Thompson","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2025,1,10]]},"reference":[{"key":"1_CR1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796820000076","volume":"31","author":"G Allais","year":"2021","unstructured":"Allais, G., Atkey, R., Chapman, J., McBride, C., McKinna, J.: A type- and scope-safe universe of syntaxes with binding: their semantics and proofs. J. Funct. Program. 31, e22 (2021)","journal-title":"J. Funct. Program."},{"key":"1_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"53","DOI":"10.1007\/978-3-662-49224-6_6","volume-title":"Software Engineering and Formal Methods","author":"M Adams","year":"2015","unstructured":"Adams, M.: Refactoring proofs with tactician. In: Bianculli, D., Calinescu, R., Rumpe, B. (eds.) SEFM 2015. LNCS, vol. 9509, pp. 53\u201367. Springer, Heidelberg (2015). https:\/\/doi.org\/10.1007\/978-3-662-49224-6_6"},{"key":"1_CR3","doi-asserted-by":"crossref","unstructured":"Brown, C., Barwell, A.D., Marquer, Y., Zendra, O., Richmond, T., Gu, C.: Semi-automatic ladderisation: improving code security through rewriting and dependent types. In: PEPM, pp. 14\u201327. ACM (2022)","DOI":"10.1145\/3498886.3502202"},{"issue":"1","key":"1_CR4","doi-asserted-by":"publisher","first-page":"44","DOI":"10.1145\/321992.321996","volume":"24","author":"RM Burstall","year":"1977","unstructured":"Burstall, R.M., Darlington, J.: A transformation system for developing recursive programs. J. ACM 24(1), 44\u201367 (1977)","journal-title":"J. ACM"},{"key":"1_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"31","DOI":"10.1007\/978-3-642-22941-1_3","volume-title":"Trends in Functional Programming","author":"C Brown","year":"2011","unstructured":"Brown, C., Li, H., Thompson, S.: An expression processor: a case study in refactoring haskell programs. In: Page, R., Horv\u00e1th, Z., Zs\u00f3k, V. (eds.) TFP 2010. LNCS, vol. 6546, pp. 31\u201349. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-22941-1_3"},{"key":"1_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"50","DOI":"10.1007\/978-3-540-30142-4_4","volume-title":"Theorem Proving in Higher Order Logics","author":"O Boite","year":"2004","unstructured":"Boite, O.: Proof reuse with extended inductive types. In: Slind, K., Bunker, A., Gopalakrishnan, G. (eds.) TPHOLs 2004. LNCS, vol. 3223, pp. 50\u201365. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-30142-4_4"},{"key":"1_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"57","DOI":"10.1007\/3-540-45315-6_4","volume-title":"Foundations of Software Science and Computation Structures","author":"G Barthe","year":"2001","unstructured":"Barthe, G., Pons, O.: Type isomorphisms and proof reuse in dependent type theory. In: Honsell, F., Miculan, M. (eds.) FoSSaCS 2001. LNCS, vol. 2030, pp. 57\u201371. Springer, Heidelberg (2001). https:\/\/doi.org\/10.1007\/3-540-45315-6_4"},{"key":"1_CR8","unstructured":"Brady, E.C.: Idris 2: quantitative type theory in practice. In: ECOOP. LIPIcs, vol. 194, pp. 9:1\u20139:26. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2021)"},{"key":"1_CR9","unstructured":"Brown, C.M.: Tool support for refactoring haskell programs. Ph.D. thesis, University of Kent, UK (2008)"},{"key":"1_CR10","doi-asserted-by":"crossref","unstructured":"Brown, C., Thompson, S.J.: Clone detection and elimination for haskell. In: PEPM, pp. 111\u2013120. ACM (2010)","DOI":"10.1145\/1706356.1706378"},{"key":"1_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"147","DOI":"10.1007\/978-3-319-03545-1_10","volume-title":"Certified Programs and Proofs","author":"C Cohen","year":"2013","unstructured":"Cohen, C., D\u00e9n\u00e8s, M., M\u00f6rtberg, A.: Refinements for free! In: Gonthier, G., Norrish, M. (eds.) CPP 2013. LNCS, vol. 8307, pp. 147\u2013162. Springer, Cham (2013). https:\/\/doi.org\/10.1007\/978-3-319-03545-1_10"},{"key":"1_CR12","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"378","DOI":"10.1007\/978-3-319-21401-6_26","volume-title":"Automated Deduction - CADE-25","author":"L de Moura","year":"2015","unstructured":"de Moura, L., Kong, S., Avigad, J., van Doorn, F., von Raumer, J.: The lean theorem prover (system description). In: Felty, A.P., Middeldorp, A. (eds.) CADE 2015. LNCS (LNAI), vol. 9195, pp. 378\u2013388. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-21401-6_26"},{"key":"1_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"83","DOI":"10.1007\/978-3-642-32347-8_7","volume-title":"Interactive Theorem Proving","author":"M D\u00e9n\u00e8s","year":"2012","unstructured":"D\u00e9n\u00e8s, M., M\u00f6rtberg, A., Siles, V.: A refinement-based approach to computational algebra in Coq. In: Beringer, L., Felty, A. (eds.) ITP 2012. LNCS, vol. 7406, pp. 83\u201398. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-32347-8_7"},{"issue":"4","key":"1_CR14","doi-asserted-by":"publisher","first-page":"440","DOI":"10.1007\/BF01211308","volume":"6","author":"P Dybjer","year":"1994","unstructured":"Dybjer, P.: Inductive Families. For. Asp. Comp. 6(4), 440\u2013465 (1994)","journal-title":"For. Asp. Comp."},{"key":"1_CR15","unstructured":"Eclipse Foundation. Eclipse (2023). http:\/\/www.eclipse.org\/"},{"key":"1_CR16","unstructured":"Fowler, M.: Refactoring - Improving the Design of Existing Code. Addison Wesley Object Technology Series. Addison-Wesley (1999)"},{"key":"1_CR17","unstructured":"Kiran Gopinathan. GopCaml: A Structural Editor for OCaml (2022). https:\/\/arxiv.org\/abs\/2207.07423"},{"key":"1_CR18","doi-asserted-by":"crossref","unstructured":"H\u00fcttel, H., Elisasen Lumholtz\u00a0Nielsen, A., Gjerulf\u00a0Sandberg, N., Lind\u00a0Andersen, C., Mikkelsen, P.: A structure editor with type-safe copy\/paste. In: IFL. ACM (2023)","DOI":"10.1145\/3587216.3587221"},{"key":"1_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"266","DOI":"10.1007\/BFb0014058","volume-title":"Typed Lambda Calculi and Applications","author":"AJC Hurkens","year":"1995","unstructured":"Hurkens, A.J.C.: A simplification of Girard\u2019s paradox. In: Dezani-Ciancaglini, M., Plotkin, G. (eds.) TLCA 1995. LNCS, vol. 902, pp. 266\u2013278. Springer, Heidelberg (1995). https:\/\/doi.org\/10.1007\/BFb0014058"},{"key":"1_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"152","DOI":"10.1007\/978-3-540-30142-4_12","volume-title":"Theorem Proving in Higher Order Logics","author":"EB Johnsen","year":"2004","unstructured":"Johnsen, E.B., L\u00fcth, C.: Theorem reuse by proof term transformation. In: Slind, K., Bunker, A., Gopalakrishnan, G. (eds.) TPHOLs 2004. LNCS, vol. 3223, pp. 152\u2013167. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-30142-4_12"},{"key":"1_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"84","DOI":"10.1007\/978-3-642-39634-2_9","volume-title":"Interactive Theorem Proving","author":"P Lammich","year":"2013","unstructured":"Lammich, P.: Automatic data refinement. In: Blazy, S., Paulin-Mohring, C., Pichardie, D. (eds.) ITP 2013. LNCS, vol. 7998, pp. 84\u201399. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-39634-2_9"},{"key":"1_CR22","unstructured":"Official Page for Language Server Protocol. https:\/\/microsoft.github.io\/language-server-protocol\/. Accessed 6 Dec 2023"},{"key":"1_CR23","unstructured":"Li, H.: Refactoring Haskell programs. Ph.D. thesis, University of Kent, UK (2006)"},{"key":"1_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"501","DOI":"10.1007\/978-3-642-28872-2_34","volume-title":"Fundamental Approaches to Software Engineering","author":"H Li","year":"2012","unstructured":"Li, H., Thompson, S.: A domain-specific language for scripting refactorings in erlang. In: de Lara, J., Zisman, A. (eds.) FASE 2012. LNCS, vol. 7212, pp. 501\u2013515. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-28872-2_34"},{"key":"1_CR25","doi-asserted-by":"crossref","unstructured":"Li, H., Thompson, S.J., Reinke, C.: The Haskell refactorer, HaRe, and its API. In: LDTA. ENTCS, vol. 141, pp. 29\u201334. Elsevier (2005)","DOI":"10.1016\/j.entcs.2005.02.053"},{"key":"1_CR26","doi-asserted-by":"crossref","unstructured":"Moon, D., Blinn, A., Omar, C.: Tylr: a tiny tile-based structure editor. In: TyDe, pp. 28\u201337. ACM (2022)","DOI":"10.1145\/3546196.3550164"},{"key":"1_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"197","DOI":"10.1007\/3-540-45842-5_13","volume-title":"Types for Proofs and Programs","author":"C McBride","year":"2002","unstructured":"McBride, C.: Elimination with a motive. In: Callaghan, P., Luo, Z., McKinna, J., Pollack, R., Pollack, R. (eds.) TYPES 2000. LNCS, vol. 2277, pp. 197\u2013216. Springer, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-45842-5_13"},{"key":"1_CR28","unstructured":"Conor McBride. Ornamental Algebras, Algebraic Ornaments (2011). https:\/\/tinyurl.com\/yc7wmb2s"},{"key":"1_CR29","unstructured":"Meta. Retrie: Haskell Refactoring Made Easy. https:\/\/engineering.fb.com\/2020\/07\/06\/open-source\/retrie\/. Accessed 7 Dec 2023"},{"key":"1_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"230","DOI":"10.1007\/978-3-642-04652-0_5","volume-title":"Advanced Functional Programming","author":"U Norell","year":"2009","unstructured":"Norell, U.: Dependently typed programming in agda. In: Koopman, P., Plasmeijer, R., Swierstra, D. (eds.) AFP 2008. LNCS, vol. 5832, pp. 230\u2013266. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-04652-0_5"},{"key":"1_CR31","unstructured":"Opdyke, W.F.: Refactoring object-oriented frameworks. Ph.D. thesis, University of Illinois Urbana-Champaign, USA (1992)"},{"key":"1_CR32","unstructured":"Paulin-Mohring, C.: Introduction to the calculus of inductive constructions. In: All about Proofs, Proofs for All, vol. 55 (2015)"},{"key":"1_CR33","unstructured":"Ringer, T.: Proof repair. Ph.D. thesis, University of Washington (2021)"},{"key":"1_CR34","unstructured":"Robert, V.: Front-end tooling for building and maintaining dependently-typed functional programs. Ph.D. thesis, University of California, San Diego (2018)"},{"key":"1_CR35","doi-asserted-by":"crossref","unstructured":"Ringer, T., Porter, R.D., Yazdani, N., Leo, J., Grossman, D.: Proof repair across type equivalences. In: PLDI, pp. 112\u2013127. ACM (2021)","DOI":"10.1145\/3453483.3454033"},{"key":"1_CR36","unstructured":"Ringer, T., Yazdani, N., Leo, J., Grossman, D.: Ornaments for proof reuse in Coq. In: ITP. LIPIcs, vol. 141, pp. 26:1\u201326:19. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2019)"},{"key":"1_CR37","doi-asserted-by":"crossref","unstructured":"Sangiorgi, D.: On the origins of bisimulation and coinduction. ACM Trans. Program. Lang. Syst. 31(4), 15:1\u201315:41 (2009)","DOI":"10.1145\/1516507.1516510"},{"key":"1_CR38","doi-asserted-by":"crossref","unstructured":"Sultana, N., Thompson, S.: Mechanical verification of refactorings. In: PEPM. ACM (2008)","DOI":"10.1145\/1328408.1328417"},{"key":"1_CR39","unstructured":"Thompson, S.J., Horp\u00e1csi, D.: Refactoring = substitution + rewriting: towards generic, language-independent refactorings. In: Eelco Visser Commemorative Symposium. OASIcs, vol. 109, pp. 26:1\u201326:9. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2023)"},{"key":"1_CR40","unstructured":"The Coq Development Team. Coq (2017). https:\/\/coq.inria.fr"},{"key":"1_CR41","doi-asserted-by":"crossref","unstructured":"Williams, T., Dagand, P.-\u00c9., R\u00e9my, D.: Ornaments in practice. In: WGP, pp. 15\u201324. ACM (2014)","DOI":"10.1145\/2633628.2633631"},{"key":"1_CR42","unstructured":"Whiteside, I.: Refactoring proofs. Ph.D. thesis, University of Edinburgh, UK (2013)"},{"key":"1_CR43","unstructured":"Wibergh, K.: Automatic Refactoring for Agda. MSc thesis, University of Gothenburg (2019)"},{"key":"1_CR44","unstructured":"Williams, A.: Refactoring functional programs with ornaments. Ph.D. thesis, Universit\u00e9 de Paris (2020)"},{"key":"1_CR45","unstructured":"Zimmermann, T., Herbelin, H.: Automatic and transparent transfer of theorems along isomorphisms in the Coq proof assistant. In: Conference on Intelligent Computer Mathematics (2015)"}],"container-title":["Lecture Notes in Computer Science","Trends in Functional Programming"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-74558-4_1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,9]],"date-time":"2025-01-09T05:03:38Z","timestamp":1736399018000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-74558-4_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025]]},"ISBN":["9783031745577","9783031745584"],"references-count":45,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-74558-4_1","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2025]]},"assertion":[{"value":"10 January 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"TFP","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Trends in Functional Programming","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"South Orange, NJ","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"USA","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2024","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"8 January 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"11 January 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"25","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"tfp2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}