Antonis Stampoulis
Adam Chlipala
Skip Abstract Section
Skip Supplemental Material SectionAbstract
We demonstrate how the framework of higher-order logic programming, as exemplified in the λProlog 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 λProlog, such as GADTs and generic programming. For our development, we make use of Makam, a new implementation of λProlog, which we introduce in tutorial style as part of our (quasi-)literate development.
Supplemental Material
- 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).Google Scholar
- Stephen Chang, Alex Knauth, and Ben Greenman. 2017. Type Systems As Macros. In Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2017). ACM, New York, NY, USA, 694–705. Google ScholarDigital Library
- Luís Damas. 1984. Type assignment in programming languages. Ph.D. Dissertation. University of Edinburgh, UK. http: //hdl.handle.net/1842/13555Google Scholar
- 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–386.Google Scholar
- Cvetan Dunchev, Ferruccio Guidi, Claudio Sacerdoti Coen, and Enrico Tassi. 2015. ELPI: fast, Embeddable, λProlog Interpreter. In Proceedings of LPAR. Suva, Fiji. https://hal.inria.fr/hal- 01176856 Google ScholarDigital Library
- Chucky Ellison, Traian Florin Şerbănuţă, and Grigore Roşu. 2008. A rewriting logic approach to type inference. In International Workshop on Algebraic Development Techniques. Springer, 135–151.Google Scholar
- 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&tid=11885 Google ScholarDigital Library
- 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–Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany, 113–128.Google Scholar
- Sebastian Fischer, Frank Huch, and Thomas Wilke. 2010. A play on regular expressions: functional pearl. In Proceeding of the 15th ACM SIGPLAN International Conference on Functional Programming, ICFP 2010, Baltimore, Maryland, USA, September 27-29, 2010. 357–368. Google ScholarDigital Library
- Andrew Gacek, Steven Holte, Gopalan Nadathur, Xiaochu Qi, and Zach Snow. 2015. The Teyjus system–version 2.Google Scholar
- Robert Harper, Furio Honsell, and Gordon Plotkin. 1993. A Framework for Defining Logics. J. ACM 40, 1 (Jan. 1993), 143–184. Google ScholarDigital Library
- Roger Hindley. 1969. The principal type-scheme of an object in combinatory logic. Trans. Amer. Math. Soc. 146 (1969), 29–60.Google Scholar
- Lennart C. L. Kats and Eelco Visser. 2010. The Spoofax Language Workbench: Rules for declarative specification of languages and IDEs. In Proceedings of the 25th Annual ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA 2010, October 17-21, 2010, Reno/Tahoe, Nevada, USA. 444–463. Google ScholarDigital Library
- Steven Keuchel, Stephanie Weirich, and Tom Schrijvers. 2016. Needle & 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–445.Google Scholar
- Oleg Kiselyov, Chung-chieh Shan, Daniel P. Friedman, and Amr Sabry. 2005. Backtracking, interleaving, and terminating monad transformers: (functional pearl). In Proceedings of the 10th ACM SIGPLAN International Conference on Functional Programming, ICFP 2005, Tallinn, Estonia, September 26-28, 2005. 192–203. Google ScholarDigital Library
- Chuck C Liang. 1995. Object-Level Substitution, Unification and Generalization in Meta-Logic. Ph.D. Dissertation. University of Pennsylvania. Google ScholarDigital Library
- Geoffrey Mainland. 2012. Explicitly heterogeneous metaprogramming with MetaHaskell. In ACM SIGPLAN International Conference on Functional Programming, ICFP’12, Copenhagen, Denmark, September 9-15, 2012. 311–322. Google ScholarDigital Library
- Dale Miller and Gopalan Nadathur. 2012. Programming with Higher-Order Logic. Cambridge University Press. Google Scholar
- Robin Milner. 1978. A theory of type polymorphism in programming. J. Comput. System Sci. 17, 3 (1978), 348 – 375.Google ScholarCross Ref
- 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–827.Google Scholar
- Gopalan Nadathur and Dustin J. Mitchell. 1999. System Description: Teyjus - A Compiler and Abstract Machine Based Implementation of λProlog. In Automated Deduction - CADE-16, 16th International Conference on Automated Deduction, Trento, Italy, July 7-10, 1999, Proceedings. 287–291. Google ScholarDigital Library
- Gopalan Nadathur and Xiaochu Qi. 2005. Optimizing the Runtime Processing of Types in Polymorphic Logic Programming Languages. In Logic for Programming, Artificial Intelligence, and Reasoning, Geoff Sutcliffe and Andrei Voronkov (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 110–124. Google ScholarDigital Library
- Aleksandar Nanevski, Frank Pfenning, and Brigitte Pientka. 2008. Contextual modal type theory. ACM Transactions on Computational Logic 9, 3 (2008), 23:1–23:49. Google ScholarDigital Library
- Frank Pfenning and Conal Elliott. 1988. Higher-order Abstract Syntax. In Proceedings of the ACM SIGPLAN 1988 Conference on Programming Language Design and Implementation (PLDI ’88). ACM, New York, NY, USA, 199–208. Google ScholarDigital Library
- Brigitte Pientka and Joshua Dunfield. 2010. Beluga: a Framework for Programming and Reasoning with Deductive Systems (System Description). In Automated Reasoning, 5th International Joint Conference, IJCAR 2010, Edinburgh, UK, July 16-19, 2010. Proceedings. 15–21. Google ScholarDigital Library
- Grigore Roşu and Traian-Florin Şerbănută. 2010. An overview of the K semantic framework. J. Log. Algebr. Program. 79, 6 (2010), 397–434.Google ScholarCross Ref
- Antonis Stampoulis. 2013. VeriML: A dependently-typed, user extensible and language-centric approach to proof assistants. Ph.D. Dissertation. Yale University.Google Scholar
- Walid Taha and Tim Sheard. 1997. Multi-stage Programming with Explicit Annotations. In Proceedings of the 1997 ACM SIGPLAN Symposium on Partial Evaluation and Semantics-based Program Manipulation (PEPM ’97). ACM, New York, NY, USA, 203–217. Google ScholarDigital Library
- Sam Tobin-Hochstadt, Vincent St-Amour, Ryan Culpepper, Matthew Flatt, and Matthias Felleisen. 2011. Languages As Libraries. In Proceedings of the 32Nd ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI ’11). ACM, New York, NY, USA, 132–141. Google ScholarDigital Library
- Jan Wielemaker, Tom Schrijvers, Markus Triska, and Torbjörn Lager. 2012. SWI-Prolog. Theory and Practice of Logic Programming 12, 1-2 (2012), 67–96. Google ScholarDigital Library
- Beta Ziliani, Derek Dreyer, Neelakantan R. Krishnaswami, Aleksandar Nanevski, and Viktor Vafeiadis. 2013. Mtac: a monad for typed tactic programming in Coq. In ACM SIGPLAN International Conference on Functional Programming, ICFP’13, Boston, MA, USA - September 25 - 27, 2013. 87–100. Google ScholarDigital Library
Index Terms
- Prototyping a functional language using higher-order logic programming: a functional pearl on learning the ways of λProlog/Makam
Recommendations
On the Effectiveness of Higher-Order Logic Programming in Language-Oriented Programming
Functional and Logic ProgrammingAbstractIn previous work we have presented [inline-graphic not available: see fulltext] , a functional language-oriented programming language with languages as first-class-citizens. Language definitions can be bound to variables, passed to and returned by ...
Extensional Higher-Order Logic Programming
We propose a purely extensional semantics for higher-order logic programming. In this semantics program predicates denote sets of ordered tuples, and two predicates are equal iff they are equal as sets. Moreover, every program has a unique minimum ...
A meta-programming approach to realizing dependently typed logic programming
PPDP '10: Proceedings of the 12th international ACM SIGPLAN symposium on Principles and practice of declarative programmingDependently typed λ-calculi such as the Logical Framework (LF) can encode relationships between terms in types and can naturally capture correspondences between formulas and their proofs. Such calculi can also be given a logic programming interpretation:...
Comments