{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:28:28Z","timestamp":1750220908805,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":57,"publisher":"ACM","license":[{"start":{"date-parts":[[2019,10,7]],"date-time":"2019-10-07T00:00:00Z","timestamp":1570406400000},"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":[[2019,10,7]]},"DOI":"10.1145\/3354166.3354177","type":"proceedings-article","created":{"date-parts":[[2019,9,24]],"date-time":"2019-09-24T12:58:36Z","timestamp":1569329916000},"page":"1-16","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Functional programming with \u03bb-tree syntax"],"prefix":"10.1145","author":[{"given":"Ulysse","family":"G\u00e9rard","sequence":"first","affiliation":[{"name":"Inria & LIX, Ecole Polytechnique, Palaiseau, France"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Dale","family":"Miller","sequence":"additional","affiliation":[{"name":"Inria & LIX, Ecole Polytechnique, Palaiseau, France"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Gabriel","family":"Scherer","sequence":"additional","affiliation":[{"name":"Inria & LIX, Ecole Polytechnique, Palaiseau, France"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2019,10,7]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF00245294"},{"key":"e_1_3_2_1_2_1","volume-title":"Mechanized Metatheory for the Masses: The POPLmark Challenge. In Theorem Proving in Higher Order Logics: 18th International Conference (LNCS). Springer, 50--65","author":"Aydemir Brian E.","year":"2005","unstructured":"Brian E. Aydemir , Aaron Bohannon , Matthew Fairbairn , J. Nathan Foster , Benjamin C. Pierce , Peter Sewell , Dimitrios Vytiniotis , Geoffrey Washburn , Stephanie Weirich , and Steve Zdancewic . 2005 . Mechanized Metatheory for the Masses: The POPLmark Challenge. In Theorem Proving in Higher Order Logics: 18th International Conference (LNCS). Springer, 50--65 . https:\/\/doi.org\/10.1007\/11541868_4 10.1007\/11541868_4 Brian E. Aydemir, Aaron Bohannon, Matthew Fairbairn, J. Nathan Foster, Benjamin C. Pierce, Peter Sewell, Dimitrios Vytiniotis, Geoffrey Washburn, Stephanie Weirich, and Steve Zdancewic. 2005. Mechanized Metatheory for the Masses: The POPLmark Challenge. In Theorem Proving in Higher Order Logics: 18th International Conference (LNCS). Springer, 50--65. https:\/\/doi.org\/10.1007\/11541868_4"},{"key":"e_1_3_2_1_3_1","first-page":"1","article-title":"Abella: A System for Reasoning about Relational Specifications","volume":"7","author":"Baelde David","year":"2014","unstructured":"David Baelde , Kaustuv Chaudhuri , Andrew Gacek , Dale Miller , Gopalan Nadathur , Alwen Tiu , and Yuting Wang . 2014 . Abella: A System for Reasoning about Relational Specifications . Journal of Formalized Reasoning 7 , 2 (2014), 1 -- 89 . https:\/\/doi.org\/10.6092\/issn.1972-5787\/4650 10.6092\/issn.1972-5787 David Baelde, Kaustuv Chaudhuri, Andrew Gacek, Dale Miller, Gopalan Nadathur, Alwen Tiu, and Yuting Wang. 2014. Abella: A System for Reasoning about Relational Specifications. Journal of Formalized Reasoning 7, 2 (2014), 1--89. https:\/\/doi.org\/10.6092\/issn.1972-5787\/4650","journal-title":"Journal of Formalized Reasoning"},{"key":"e_1_3_2_1_4_1","article-title":"The Locally Nameless Representation","author":"Chargu\u00e9raud Arthur","year":"2011","unstructured":"Arthur Chargu\u00e9raud . 2011 . The Locally Nameless Representation . Journal of Automated Reasoning ( May 2011), 1--46. https:\/\/doi.org\/10.1007\/s10817-011-9225-2 10.1007\/s10817-011-9225-2 Arthur Chargu\u00e9raud. 2011. The Locally Nameless Representation. Journal of Automated Reasoning (May 2011), 1--46. https:\/\/doi.org\/10.1007\/s10817-011-9225-2","journal-title":"Journal of Automated Reasoning"},{"key":"e_1_3_2_1_5_1","volume-title":"20th International Conference (LNCS), Bart Demoen and Vladimir Lifschitz (Eds.)","volume":"3132","author":"Cheney James","year":"2004","unstructured":"James Cheney and Christian Urban . 2004 . Alpha-Prolog: A Logic Programming Language with Names, Binding, and Alpha-Equivalence. In Logic Programming , 20th International Conference (LNCS), Bart Demoen and Vladimir Lifschitz (Eds.) , Vol. 3132 . Springer, 269--283. https:\/\/doi.org\/10.1007\/978-3-540-27775-0_19 10.1007\/978-3-540-27775-0_19 James Cheney and Christian Urban. 2004. Alpha-Prolog: A Logic Programming Language with Names, Binding, and Alpha-Equivalence. In Logic Programming, 20th International Conference (LNCS), Bart Demoen and Vladimir Lifschitz (Eds.), Vol. 3132. Springer, 269--283. https:\/\/doi.org\/10.1007\/978-3-540-27775-0_19"},{"key":"e_1_3_2_1_6_1","volume-title":"Proceedings of the Eigth International Conference","author":"Cheng Anthony S. K.","year":"1991","unstructured":"Anthony S. K. Cheng , Peter J. Robinson , and John Staples . 1991 . Higher Level Meta Programming in Qu-Prolog 3: 0. In Logic Programming , Proceedings of the Eigth International Conference , Paris, France , June 24-28, 1991, Koichi Furukawa (Ed.). MIT Press, 285--298. Anthony S. K. Cheng, Peter J. Robinson, and John Staples. 1991. Higher Level Meta Programming in Qu-Prolog 3: 0. In Logic Programming, Proceedings of the Eigth International Conference, Paris, France, June 24-28, 1991, Koichi Furukawa (Ed.). MIT Press, 285--298."},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/1411204.1411226"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.2307\/2266170"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1016\/1385-7258(72)90034-0"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.5555\/645892.671587"},{"key":"e_1_3_2_1_12_1","volume-title":"Claudio Sacerdoti Coen, and Enrico Tassi","author":"Dunchev Cvetan","year":"2015","unstructured":"Cvetan Dunchev , Ferruccio Guidi , Claudio Sacerdoti Coen, and Enrico Tassi . 2015 . ELPI : Fast, Embeddable, \u03bb Prolog Interpreter. In Logic for Programming, Artificial Intelligence, and Reasoning - 20th International Conference, LPAR-20 2015, Suva, Fiji, November 24-28, 2015, Proceedings (LNCS), Martin Davis, Ansgar Fehnker, Annabelle McIver, and Andrei Voronkov (Eds.), Vol. 9450 . Springer , 460--468. https:\/\/doi.org\/10.1007\/978-3-662-48899-7_32 10.1007\/978-3-662-48899-7_32 Cvetan Dunchev, Ferruccio Guidi, Claudio Sacerdoti Coen, and Enrico Tassi. 2015. ELPI: Fast, Embeddable, \u03bb Prolog Interpreter. In Logic for Programming, Artificial Intelligence, and Reasoning - 20th International Conference, LPAR-20 2015, Suva, Fiji, November 24-28, 2015, Proceedings (LNCS), Martin Davis, Ansgar Fehnker, Annabelle McIver, and Andrei Voronkov (Eds.), Vol. 9450. Springer, 460--468. https:\/\/doi.org\/10.1007\/978-3-662-48899-7_32"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-015-9327-3"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54434-1_19"},{"volume-title":"14th Symp. on Logic in Computer Science. IEEE Computer Society Press, 214--224","author":"Gabbay M. J.","key":"e_1_3_2_1_15_1","unstructured":"M. J. Gabbay and A. M. Pitts . 1999. A new approach to abstract syntax involving binders . In 14th Symp. on Logic in Computer Science. IEEE Computer Society Press, 214--224 . M. J. Gabbay and A. M. Pitts. 1999. A new approach to abstract syntax involving binders. In 14th Symp. on Logic in Computer Science. IEEE Computer Society Press, 214--224."},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2008.33"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2010.09.004"},{"key":"e_1_3_2_1_20_1","unstructured":"Ulysse G\u00e9rard Dale Miller and Gabriel Scherer. 2018. Try MLTS Online. https:\/\/trymlts.github.io\/.  Ulysse G\u00e9rard Dale Miller and Gabriel Scherer. 2018. Try MLTS Online. https:\/\/trymlts.github.io\/."},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-57826-9_152"},{"key":"e_1_3_2_1_22_1","volume-title":"Wadsworth","author":"Gordon Michael J.","year":"1979","unstructured":"Michael J. Gordon , Arthur J. Milner , and Christopher P . Wadsworth . 1979 . Edinburgh LCF: A Mechanised Logic of Computation. LNCS, Vol. 78 . Springer . Michael J. Gordon, Arthur J. Milner, and Christopher P. Wadsworth. 1979. Edinburgh LCF: A Mechanised Logic of Computation. LNCS, Vol. 78. Springer."},{"volume-title":"Proceedings of the International Workshop on the HOL Theorem Proving System and its Applications, Myla Archer, Jeffrey J","author":"Gordon Michael J. C.","key":"e_1_3_2_1_23_1","unstructured":"Michael J. C. Gordon . 1991. Introduction to the HOL System . In Proceedings of the International Workshop on the HOL Theorem Proving System and its Applications, Myla Archer, Jeffrey J . Joyce, Karl N. Levitt, and Phillip J. Windley (Eds.). IEEE Computer Society , 2--3. Michael J. C. Gordon. 1991. Introduction to the HOL System. In Proceedings of the International Workshop on the HOL Theorem Proving System and its Applications, Myla Archer, Jeffrey J. Joyce, Karl N. Levitt, and Phillip J. Windley (Eds.). IEEE Computer Society, 2--3."},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/138027.138060"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03359-9_4"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(75)90011-0"},{"key":"e_1_3_2_1_27_1","unstructured":"js-of-ocaml 2018. Js_of_ocaml. http:\/\/ocsigen.org\/js_of_ocaml\/.  js-of-ocaml 2018. Js_of_ocaml. http:\/\/ocsigen.org\/js_of_ocaml\/."},{"key":"e_1_3_2_1_28_1","volume-title":"Natural Semantics. In Proceedings of the Symposium on Theoretical Aspects of Computer Science (LNCS), Franz-Josef Brandenburg, Guy Vidal-Naquet, and Martin Wirsing (Eds.)","volume":"247","author":"Kahn Gilles","year":"1987","unstructured":"Gilles Kahn . 1987 . Natural Semantics. In Proceedings of the Symposium on Theoretical Aspects of Computer Science (LNCS), Franz-Josef Brandenburg, Guy Vidal-Naquet, and Martin Wirsing (Eds.) , Vol. 247 . Springer, 22--39. Gilles Kahn. 1987. Natural Semantics. In Proceedings of the Symposium on Theoretical Aspects of Computer Science (LNCS), Franz-Josef Brandenburg, Guy Vidal-Naquet, and Martin Wirsing (Eds.), Vol. 247. Springer, 22--39."},{"volume-title":"Proceedings of the 14th ACM SIGPLAN International Conference on Functional Programming (ICFP '09)","author":"Daniel","key":"e_1_3_2_1_29_1","unstructured":"Daniel R. Licata and Robert Harper. 2009. A Universe of Binding and Computation . In Proceedings of the 14th ACM SIGPLAN International Conference on Functional Programming (ICFP '09) . ACM, New York, NY, USA, 123--134. https:\/\/doi.org\/10.1145\/1596550.1596571 10.1145\/1596550.1596571 Daniel R. Licata and Robert Harper. 2009. A Universe of Binding and Computation. In Proceedings of the 14th ACM SIGPLAN International Conference on Functional Programming (ICFP '09). ACM, New York, NY, USA, 123--134. https:\/\/doi.org\/10.1145\/1596550.1596571"},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/1017472.1017477"},{"key":"e_1_3_2_1_31_1","volume-title":"Proceedings of the Logical Frameworks BRA Workshop","author":"Miller Dale","year":"1990","unstructured":"Dale Miller . 1990 . An Extension to ML to Handle Bound Variables in Data Structures: Preliminary Report . In Proceedings of the Logical Frameworks BRA Workshop . Antibes, France, 323--335. http:\/\/www.lix.polytechnique.fr\/Labo\/Dale.Miller\/papers\/mll.pdf Available as UPenn CIS technical report MS-CIS-90-59. Dale Miller. 1990. An Extension to ML to Handle Bound Variables in Data Structures: Preliminary Report. In Proceedings of the Logical Frameworks BRA Workshop. Antibes, France, 323--335. http:\/\/www.lix.polytechnique.fr\/Labo\/Dale.Miller\/papers\/mll.pdf Available as UPenn CIS technical report MS-CIS-90-59."},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/1.4.497"},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1016\/0747-7171(92)90011-R"},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(96)00045-X"},{"key":"e_1_3_2_1_35_1","volume-title":"18th International Conference on Computer Science Logic (CSL) 2004 (LNCS), Jerzy Marcinkowski and Andrzej Tarlecki (Eds.)","volume":"3210","author":"Miller Dale","year":"2004","unstructured":"Dale Miller . 2004 . Bindings, mobility of bindings, and the ∇-quantifier . In 18th International Conference on Computer Science Logic (CSL) 2004 (LNCS), Jerzy Marcinkowski and Andrzej Tarlecki (Eds.) , Vol. 3210 . 24. https:\/\/doi.org\/10.1007\/978-3-540-30124-0_4 10.1007\/978-3-540-30124-0_4 Dale Miller. 2004. Bindings, mobility of bindings, and the ∇-quantifier. In 18th International Conference on Computer Science Logic (CSL) 2004 (LNCS), Jerzy Marcinkowski and Andrzej Tarlecki (Eds.), Vol. 3210. 24. https:\/\/doi.org\/10.1007\/978-3-540-30124-0_4"},{"key":"e_1_3_2_1_36_1","article-title":"Mechanized Metatheory Revisited","author":"Miller Dale","year":"2018","unstructured":"Dale Miller . 2018 . Mechanized Metatheory Revisited . Journal of Automated Reasoning (04 Oct. 2018). https:\/\/doi.org\/10.1007\/s10817-018-9483-3 10.1007\/s10817-018-9483-3 Dale Miller. 2018. Mechanized Metatheory Revisited. Journal of Automated Reasoning (04 Oct. 2018). https:\/\/doi.org\/10.1007\/s10817-018-9483-3","journal-title":"Journal of Automated Reasoning (04"},{"volume-title":"Programming with Higher-Order Logic","author":"Miller Dale","key":"e_1_3_2_1_37_1","unstructured":"Dale Miller and Gopalan Nadathur . 2012. Programming with Higher-Order Logic . Cambridge University Press . https:\/\/doi.org\/10.1017\/CBO9781139021326 10.1017\/CBO9781139021326 Dale Miller and Gopalan Nadathur. 2012. Programming with Higher-Order Logic. Cambridge University Press. https:\/\/doi.org\/10.1017\/CBO9781139021326"},{"key":"e_1_3_2_1_38_1","volume-title":"Foundational Aspects of Syntax. Comput. Surveys 31 (Sept","author":"Miller Dale","year":"1999","unstructured":"Dale Miller and Catuscia Palamidessi . 1999. Foundational Aspects of Syntax. Comput. Surveys 31 (Sept . 1999 ). Dale Miller and Catuscia Palamidessi. 1999. Foundational Aspects of Syntax. Comput. Surveys 31 (Sept. 1999)."},{"key":"e_1_3_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/1094622.1094628"},{"key":"e_1_3_2_1_40_1","volume-title":"Fifth International Logic Programming Conference. MIT Press","author":"Nadathur Gopalan","year":"1988","unstructured":"Gopalan Nadathur and Dale Miller . 1988 . An Overview of \u03bb Prolog . In Fifth International Logic Programming Conference. MIT Press , Seattle, 810--827. http:\/\/www.lix.polytechnique.fr\/Labo\/Dale.Miller\/papers\/iclp88.pdf Gopalan Nadathur and Dale Miller. 1988. An Overview of \u03bb Prolog. In Fifth International Logic Programming Conference. MIT Press, Seattle, 810--827. http:\/\/www.lix.polytechnique.fr\/Labo\/Dale.Miller\/papers\/iclp88.pdf"},{"key":"e_1_3_2_1_41_1","volume-title":"Functional Unification of Higher-Order Patterns. In 8th Symp. on Logic in Computer Science, M. Vardi (Ed.). IEEE, 64--74","author":"Nipkow Tobias","year":"1993","unstructured":"Tobias Nipkow . 1993 . Functional Unification of Higher-Order Patterns. In 8th Symp. on Logic in Computer Science, M. Vardi (Ed.). IEEE, 64--74 . Tobias Nipkow. 1993. Functional Unification of Higher-Order Patterns. In 8th Symp. on Logic in Computer Science, M. Vardi (Ed.). IEEE, 64--74."},{"key":"e_1_3_2_1_42_1","unstructured":"OCaml. 2018. http:\/\/ocaml.org\/.  OCaml. 2018. http:\/\/ocaml.org\/."},{"key":"e_1_3_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF00248324"},{"key":"e_1_3_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0030541"},{"key":"e_1_3_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/53990.54010"},{"key":"e_1_3_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-48660-7_14"},{"key":"e_1_3_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14203-1_2"},{"key":"e_1_3_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0890-5401(03)00138-X"},{"key":"e_1_3_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1007\/10722010_15"},{"key":"e_1_3_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78739-6_7"},{"key":"e_1_3_2_1_51_1","volume-title":"International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP","author":"Poswolsky Adam","year":"2008","unstructured":"Adam Poswolsky and Carsten Sch\u00fcrmann . 2008 . System Description: Delphin - A Functional Programming Language for Deductive Systems , In International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP 2008), A. Abel and C. Urban (Eds.). Electr. Notes Theor. Comput. Sci. 228, 113--120. Adam Poswolsky and Carsten Sch\u00fcrmann. 2008. System Description: Delphin - A Functional Programming Language for Deductive Systems, In International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP 2008), A. Abel and C. Urban (Eds.). Electr. Notes Theor. Comput. Sci. 228, 113--120."},{"key":"e_1_3_2_1_52_1","volume-title":"Proceedings of the ACM-SIGPLAN Workshop on ML (ML 2005)","volume":"148","author":"Pottier Fran\u00e7ois","year":"2006","unstructured":"Fran\u00e7ois Pottier . 2006 . An Overview of C α ml . In Proceedings of the ACM-SIGPLAN Workshop on ML (ML 2005) (Electr. Notes Theor. Comput. Sci.) , Vol. 148 . 27--52. https:\/\/doi.org\/10.1016\/j.entcs.2005.11.039 10.1016\/j.entcs.2005.11.039 Fran\u00e7ois Pottier. 2006. An Overview of C α ml. In Proceedings of the ACM-SIGPLAN Workshop on ML (ML 2005) (Electr. Notes Theor. Comput. Sci.), Vol. 148. 27--52. https:\/\/doi.org\/10.1016\/j.entcs.2005.11.039"},{"key":"e_1_3_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2007.44"},{"key":"e_1_3_2_1_54_1","unstructured":"Xiaochu Qi Andrew Gacek Steven Holte Gopalan Nadathur and Zach Snow. 2015. The Teyjus System - Version 2. http:\/\/teyjus.cs.umn.edu\/ http:\/\/teyjus.cs.umn.edu\/.  Xiaochu Qi Andrew Gacek Steven Holte Gopalan Nadathur and Zach Snow. 2015. The Teyjus System - Version 2. http:\/\/teyjus.cs.umn.edu\/ http:\/\/teyjus.cs.umn.edu\/."},{"key":"e_1_3_2_1_55_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(96)00075-8"},{"key":"e_1_3_2_1_56_1","doi-asserted-by":"publisher","DOI":"10.1007\/11417170_25"},{"volume-title":"The Seventeen Provers of the World (LNCS)","author":"Schwichtenberg Helmut","key":"e_1_3_2_1_57_1","unstructured":"Helmut Schwichtenberg . 2006. Minlog . In The Seventeen Provers of the World (LNCS) , Freek Wiedijk (Ed.), Vol. 3600 . Springer , 151--157. https:\/\/doi.org\/10.1007\/11542384_19 10.1007\/11542384_19 Helmut Schwichtenberg. 2006. Minlog. In The Seventeen Provers of the World (LNCS), Freek Wiedijk (Ed.), Vol. 3600. Springer, 151--157. https:\/\/doi.org\/10.1007\/11542384_19"},{"key":"e_1_3_2_1_58_1","volume-title":"Proceedings, Fourth Annual Princeton Conference on Information Sciences and Systems","author":"Scott Dana","year":"1970","unstructured":"Dana Scott . 1970 . Outline of a Mathematical Theory of Computation . In Proceedings, Fourth Annual Princeton Conference on Information Sciences and Systems . Princeton University, 169--176. Also, Programming Research Group Technical Monograph PRG-2, Oxford University. Dana Scott. 1970. Outline of a Mathematical Theory of Computation. In Proceedings, Fourth Annual Princeton Conference on Information Sciences and Systems. Princeton University, 169--176. Also, Programming Research Group Technical Monograph PRG-2, Oxford University."},{"key":"e_1_3_2_1_59_1","volume-title":"FreshML: Programming with Binders Made Simple. In Eighth ACM SIGPLAN International Conference on Functional Programming (ICFP","author":"Shinwell M. R.","year":"2003","unstructured":"M. R. Shinwell , A. M. Pitts , and M. J. Gabbay . 2003 . FreshML: Programming with Binders Made Simple. In Eighth ACM SIGPLAN International Conference on Functional Programming (ICFP 2003 ), Uppsala, Sweden. ACM Press, 263--274. M. R. Shinwell, A. M. Pitts, and M. J. Gabbay. 2003. FreshML: Programming with Binders Made Simple. In Eighth ACM SIGPLAN International Conference on Functional Programming (ICFP 2003), Uppsala, Sweden. ACM Press, 263--274."},{"key":"e_1_3_2_1_60_1","doi-asserted-by":"publisher","DOI":"10.1145\/2505879.2505889"}],"event":{"name":"PPDP '19: Principles and Practice of Programming Languages 2019","sponsor":["Sony Sony Corporation"],"location":"Porto Portugal","acronym":"PPDP '19"},"container-title":["Proceedings of the 21st International Symposium on Principles and Practice of Declarative Programming"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3354166.3354177","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3354166.3354177","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T23:44:56Z","timestamp":1750203896000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3354166.3354177"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,10,7]]},"references-count":57,"alternative-id":["10.1145\/3354166.3354177","10.1145\/3354166"],"URL":"https:\/\/doi.org\/10.1145\/3354166.3354177","relation":{},"subject":[],"published":{"date-parts":[[2019,10,7]]},"assertion":[{"value":"2019-10-07","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}