{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:56:39Z","timestamp":1750308999037,"version":"3.41.0"},"reference-count":28,"publisher":"Association for Computing Machinery (ACM)","issue":"ICFP","license":[{"start":{"date-parts":[[2018,7,30]],"date-time":"2018-07-30T00:00:00Z","timestamp":1532908800000},"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-1217501"],"award-info":[{"award-number":["CCF-1217501"]}],"id":[{"id":"10.13039\/100000001","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":[[2018,7,30]]},"abstract":"<jats:p>\n            We demonstrate how the framework of\n            <jats:italic>higher-order logic programming<\/jats:italic>\n            , as exemplified in the \u03bbProlog language design, is a prime vehicle for rapid prototyping of implementations for programming languages with sophisticated type systems. We present the literate development of a type checker for a language with a number of complicated features, culminating in a standard ML-style core with algebraic datatypes and type generalization, extended with staging constructs that are generic over a separately defined language of terms. We add each new feature in sequence, with little to no changes to existing code. Scaling the higher-order logic programming approach to this setting required us to develop approaches to challenges like complex variable binding patterns in object languages and performing generic structural traversals of code, making use of novel constructions in the setting of \u03bbProlog, such as GADTs and generic programming. For our development, we make use of Makam, a new implementation of \u03bbProlog, which we introduce in tutorial style as part of our (quasi-)literate development.\n          <\/jats:p>","DOI":"10.1145\/3236788","type":"journal-article","created":{"date-parts":[[2018,7,31]],"date-time":"2018-07-31T19:41:18Z","timestamp":1533066078000},"page":"1-30","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["Prototyping a functional language using higher-order logic programming: a functional pearl on learning the ways of \u03bbProlog\/Makam"],"prefix":"10.1145","volume":"2","author":[{"given":"Antonis","family":"Stampoulis","sequence":"first","affiliation":[{"name":"Originate, USA"}]},{"given":"Adam","family":"Chlipala","sequence":"additional","affiliation":[{"name":"Massachusetts Institute of Technology, USA"}]}],"member":"320","published-online":{"date-parts":[[2018,7,30]]},"reference":[{"key":"e_1_2_2_1_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). 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).","journal-title":"Journal of Formalized Reasoning"},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009886"},{"key":"e_1_2_2_4_1","volume-title":"Proceedings of the 1991 International Logic Programming Symposium. MIT Press, 372\u2013386","author":"Dietzen Scott","year":"1991","unstructured":"Scott Dietzen and Frank Pfenning . 1991 . A Declarative Alternative to \"Assert\" in Logic Programming . In Proceedings of the 1991 International Logic Programming Symposium. MIT Press, 372\u2013386 . Scott Dietzen and Frank Pfenning. 1991. A Declarative Alternative to \"Assert\" in Logic Programming. In Proceedings of the 1991 International Logic Programming Symposium. MIT Press, 372\u2013386."},{"key":"e_1_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-48899-7_32"},{"key":"e_1_2_2_6_1","volume-title":"International Workshop on Algebraic Development Techniques. Springer, 135\u2013151","author":"Ellison Chucky","year":"2008","unstructured":"Chucky Ellison , Traian Florin \u015eerb\u0103nu\u0163\u0103 , and Grigore Ro\u015fu . 2008 . A rewriting logic approach to type inference . In International Workshop on Algebraic Development Techniques. Springer, 135\u2013151 . Chucky Ellison, Traian Florin \u015eerb\u0103nu\u0163\u0103, and Grigore Ro\u015fu. 2008. A rewriting logic approach to type inference. In International Workshop on Algebraic Development Techniques. Springer, 135\u2013151."},{"key":"e_1_2_2_7_1","volume-title":"Robert Bruce Findler, and Matthew Flatt","author":"Felleisen Matthias","year":"2009","unstructured":"Matthias Felleisen , Robert Bruce Findler, and Matthew Flatt . 2009 . Semantics Engineering with PLT Redex. MIT Press . http:\/\/mitpress.mit.edu\/catalog\/item\/default.asp?ttype=2&amp;tid=11885 Matthias Felleisen, Robert Bruce Findler, and Matthew Flatt. 2009. Semantics Engineering with PLT Redex. MIT Press. http:\/\/mitpress.mit.edu\/catalog\/item\/default.asp?ttype=2&amp;tid=11885"},{"key":"e_1_2_2_8_1","volume-title":"Matthew Flatt, Shriram Krishnamurthi, Eli Barzilay, Jay McCarthy, and Sam TobinHochstadt.","author":"Felleisen Matthias","year":"2015","unstructured":"Matthias Felleisen , Robert Bruce Findler , Matthew Flatt, Shriram Krishnamurthi, Eli Barzilay, Jay McCarthy, and Sam TobinHochstadt. 2015 . The Racket Manifesto. In 1st Summit on Advances in Programming Languages (SNAPL 2015) (Leibniz International Proceedings in Informatics (LIPIcs)), Thomas Ball, Rastislav Bodik, Shriram Krishnamurthi, Benjamin S. Lerner, and Greg Morrisett (Eds.), Vol. 32 . Schloss Dagstuhl\u2013Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany , 113\u2013128. Matthias Felleisen, Robert Bruce Findler, Matthew Flatt, Shriram Krishnamurthi, Eli Barzilay, Jay McCarthy, and Sam TobinHochstadt. 2015. The Racket Manifesto. In 1st Summit on Advances in Programming Languages (SNAPL 2015) (Leibniz International Proceedings in Informatics (LIPIcs)), Thomas Ball, Rastislav Bodik, Shriram Krishnamurthi, Benjamin S. Lerner, and Greg Morrisett (Eds.), Vol. 32. Schloss Dagstuhl\u2013Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany, 113\u2013128."},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/1863543.1863594"},{"key":"e_1_2_2_10_1","unstructured":"Andrew Gacek Steven Holte Gopalan Nadathur Xiaochu Qi and Zach Snow. 2015. The Teyjus system\u2013version 2.  Andrew Gacek Steven Holte Gopalan Nadathur Xiaochu Qi and Zach Snow. 2015. The Teyjus system\u2013version 2."},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/138027.138060"},{"key":"e_1_2_2_12_1","first-page":"29","article-title":"The principal type-scheme of an object in combinatory logic","volume":"146","author":"Hindley Roger","year":"1969","unstructured":"Roger Hindley . 1969 . The principal type-scheme of an object in combinatory logic . Trans. Amer. Math. Soc. 146 (1969), 29 \u2013 60 . Roger Hindley. 1969. The principal type-scheme of an object in combinatory logic. Trans. Amer. Math. Soc. 146 (1969), 29\u201360.","journal-title":"Trans. Amer. Math. Soc."},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/1869459.1869497"},{"key":"e_1_2_2_14_1","volume-title":"ESOP 2016, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016, Eindhoven, The Netherlands, April 2-8, 2016, Proceedings. 419\u2013445","author":"Keuchel Steven","year":"2016","unstructured":"Steven Keuchel , Stephanie Weirich , and Tom Schrijvers . 2016 . Needle &amp; Knot: Binder Boilerplate Tied Up. In Programming Languages and Systems - 25th European Symposium on Programming , ESOP 2016, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016, Eindhoven, The Netherlands, April 2-8, 2016, Proceedings. 419\u2013445 . Steven Keuchel, Stephanie Weirich, and Tom Schrijvers. 2016. Needle &amp; Knot: Binder Boilerplate Tied Up. In Programming Languages and Systems - 25th European Symposium on Programming, ESOP 2016, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016, Eindhoven, The Netherlands, April 2-8, 2016, Proceedings. 419\u2013445."},{"key":"e_1_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/1086365.1086390"},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/2364527.2364572"},{"volume-title":"Programming with Higher-Order Logic","author":"Miller Dale","key":"e_1_2_2_18_1","unstructured":"Dale Miller and Gopalan Nadathur . 2012. Programming with Higher-Order Logic . Cambridge University Press . Dale Miller and Gopalan Nadathur. 2012. Programming with Higher-Order Logic. Cambridge University Press."},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(78)90014-4"},{"key":"e_1_2_2_20_1","volume-title":"Proceedings of the Fifth International Conference on Logic Programming","author":"Nadathur Gopalan","year":"1988","unstructured":"Gopalan Nadathur and Dale Miller . 1988 . An Overview of Lambda-PROLOG . In Proceedings of the Fifth International Conference on Logic Programming , Seattle, Washington , August 15-19, 1988 (2 Volumes). 810\u2013827. Gopalan Nadathur and Dale Miller. 1988. An Overview of Lambda-PROLOG. In Proceedings of the Fifth International Conference on Logic Programming, Seattle, Washington, August 15-19, 1988 (2 Volumes). 810\u2013827."},{"volume-title":"16th International Conference on Automated Deduction, Trento, Italy, July 7-10, 1999, Proceedings. 287\u2013291","author":"Nadathur Gopalan","key":"e_1_2_2_21_1","unstructured":"Gopalan Nadathur and Dustin J. Mitchell . 1999. System Description: Teyjus - A Compiler and Abstract Machine Based Implementation of \u03bbProlog. In Automated Deduction - CADE-16 , 16th International Conference on Automated Deduction, Trento, Italy, July 7-10, 1999, Proceedings. 287\u2013291 . Gopalan Nadathur and Dustin J. Mitchell. 1999. System Description: Teyjus - A Compiler and Abstract Machine Based Implementation of \u03bbProlog. In Automated Deduction - CADE-16, 16th International Conference on Automated Deduction, Trento, Italy, July 7-10, 1999, Proceedings. 287\u2013291."},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/11591191_9"},{"key":"e_1_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/1352582.1352591"},{"key":"e_1_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/53990.54010"},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14203-1_2"},{"key":"e_1_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlap.2010.03.012"},{"key":"e_1_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/258993.259019"},{"key":"e_1_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/1993498.1993514"},{"key":"e_1_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1017\/S1471068411000494"},{"key":"e_1_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/2500365.2500579"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3236788","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3236788","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3236788","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T21:41:28Z","timestamp":1750282888000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3236788"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,7,30]]},"references-count":28,"journal-issue":{"issue":"ICFP","published-print":{"date-parts":[[2018,7,30]]}},"alternative-id":["10.1145\/3236788"],"URL":"https:\/\/doi.org\/10.1145\/3236788","relation":{},"ISSN":["2475-1421"],"issn-type":[{"type":"electronic","value":"2475-1421"}],"subject":[],"published":{"date-parts":[[2018,7,30]]},"assertion":[{"value":"2018-07-30","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}