Compiler Construction in Higher Order Logic Programming

  • Chuck C. Liang
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2257)


This paper describes a general method of compiler implementation using higher order abstract syntax and logic programming. A working compiler written in λProlog is used to demonstrate this method. Various stages of compilation are formulated as higher order logic programming including parsing and the generation of higher order representations, type checking, intermediate representation in continuationpassing style, and machine-dependent code generation. The performance overhead of using higher order representations is also addressed.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    M. Abadi, L. Cardelli, P. Curien, and J. Levy. Explicit substitutions. Journal of Functional Programming, 1(4):375–416, 1991.zbMATHMathSciNetCrossRefGoogle Scholar
  2. 2.
    A. W. Appel. Compiling with Continuations. Cambridge University Press, 1992.Google Scholar
  3. 3.
    A. W. Appel. Modern Compiler Implementation in ML. Cambridge University Press, 1998.Google Scholar
  4. 4.
    J. Cohen and T. Hickey. Parsing and compiling using Prolog. ACM Transactions on Programming Languages and Systems, 9(2):125–163, 1987.CrossRefGoogle Scholar
  5. 5.
    L. Damas and R. Milner. Principal type-schemes for functional programs. In Ninth Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 207–212, January 1982.Google Scholar
  6. 6.
    O. Danvy. Back to direct style. Science of Computer Programming, 22(3):183–195, 1994.zbMATHCrossRefMathSciNetGoogle Scholar
  7. 7.
    O. Danvy, B. Dzafic, and F. Pfenning. On proving syntactic properties of CPS programs. In Proceedings of the Third International Workshop on Higher Order Operational Techniques in Semantics, September 1999.Google Scholar
  8. 8.
    A. Felty. Defining object-level parsers in λProlog. In Proceedings of the Workshop on the λProlog Programming Language, 1992. Department of Computer and Information Science, University of Pennsylvania, Technical Report MS-CIS-92-86.Google Scholar
  9. 9.
    M. Fischer. Lambda calculus schemata. In ACM Conference on Proving Assertions about Programs, SIGPLAN Notices 7, number 1, pages 104–109, 1972.Google Scholar
  10. 10.
    C. Flanagan, A. Sabry, B. Duba, and M. Felleisen. The essence of compiling with continuations. In ACM SIGPLAN Conference on Programming Language Design and Implementation, pages 237–247. ACM Press, 1993.Google Scholar
  11. 11.
    R. Floyd. Bounded context syntactic analysis. Communications of the ACM, 7(2):62–67, 1964.zbMATHCrossRefGoogle Scholar
  12. 12.
    S. L. Graham. On bounded right context languages and grammars. SIAM Journal on Computing, 3(3):224–254, 1974.zbMATHCrossRefMathSciNetGoogle Scholar
  13. 13.
    J. Hannan. Investigating a Proof-Theoretic Meta-Language for Functional Programs. PhD thesis, University of Pennsylvania, August 1990.Google Scholar
  14. 14.
    J. Hannan and D. Miller. Uses of higher-order unification for implementing program transformers. In Fifth International Logic Programming Conference, pages 942–959, Seattle, Washington, August 1988. MIT Press.Google Scholar
  15. 15.
    J. Hannan and F. Pfenning. Compiler verification in LF. In Seventh Annual IEEE Symposium on Logic in Computer Science, Santa Cruz, California, June 1992. IEEE Computer Society Press.Google Scholar
  16. 16.
    M. Harrison and I. Havel. On the parsing of deterministic languages. Journal of the ACM, 21(4):525–548, 1974.zbMATHCrossRefMathSciNetGoogle Scholar
  17. 17.
    J. Hodas and D. Miller. Logic programming in a fragment of intuitionistic linear logic. Information and Computation, 110(2):327–365, 1994.zbMATHCrossRefMathSciNetGoogle Scholar
  18. 18.
    Gérard Huet. A unification algorithm for typed λ-calculus. Theoretical Computer Science, 1:27–57, 1975.CrossRefMathSciNetGoogle Scholar
  19. 19.
    S. Le Huitouze, P. Louvet, and O. Ridoux. Logic grammars and λProlog. In David S. Warren, editor, Proceedings of the Tenth International Conference on Logic Programming, pages 64–79. MIT Press, 1993.Google Scholar
  20. 20.
    D. E. Knuth. On the translation of languages from left to right. Information and Control, 8(6):607–639, 1965.CrossRefMathSciNetGoogle Scholar
  21. 21.
    D. Kranz, R. Kelsey, J. Rees, P. Hudak, J. Philbin, and N. Adams. ORBIT: An optimizing compiler for Scheme. In SIGPLAN 1986 Symposium on Compiler Construction, SIGPLAN Notices 21, number 7, pages 219–233, 1986.Google Scholar
  22. 22.
    C. Liang. Let-polymorphism and eager type schemes. In TAPSOFT’ 97: Theory and Practice of Software Development, pages 490–501. Springer Verlag LNCS Vol. 1214, 1997.CrossRefGoogle Scholar
  23. 23.
    C. Liang. A deterministic shift-reduce parser generator for a logic programming language. In Computational Logic-CL 2000, Springer-Verlag LNAI no. 1861, pages 1315–1329, July 2000.Google Scholar
  24. 24.
    C. Liang and G. Nadathur. Trade-offs in the intensional representation of lambda terms. Submitted for publication.Google Scholar
  25. 25.
    D. Miller. A logic programming language with λ-abstraction, function variables, and simple unification. Journal of Logic and Computation, 1(4):497–536, 1991.zbMATHCrossRefMathSciNetGoogle Scholar
  26. 26.
    D. Miller. Unification of simply typed lambda-terms as logic programming. In 8th International Logic Programming Conference, pages 255–269. MIT Press, 1991.Google Scholar
  27. 27.
    D. Miller. Abstract syntax for variable binders: An overview. In Computational Logic-CL 2000, Springer-Verlag LNAI no. 1861, pages 239–253, July 2000.Google Scholar
  28. 28.
    D. Miller, G. Nadathur, F. Pfenning, and A. Scedrov. Uniform proofs as a foundation for logic programming. Annals of Pure and Applied Logic, 51:125–157, 1991.CrossRefMathSciNetzbMATHGoogle Scholar
  29. 29.
    G. Nadathur. An explicit substitution notation in a ?Prolog implementation. Technical Report TR-98-01, Department of Computer Science, University of Chicago, January 1998. Also appears in the Proceedings of the First InternationalWorkshop on Explicit Substitutions, Tsukuba, Japan, March1998.Google Scholar
  30. 30.
    G. Nadathur. A fine-grained notation for lambda terms and its use in intensional operations. Journal of Functional and Logic Programming, 1999(2), March1999.Google Scholar
  31. 31.
    G. Nadathur and D. Miller. An Overview of λProlog. In Fifth International Logic Programming Conference, pages 810–827. MIT Press, August 1988.Google Scholar
  32. 32.
    G. Nadathur and D. Miller. Higher-order logic programming. In D. Gabbay, C. Hogger, and A. Robinson, editors, Handbook of Logic in Artificial Intelligence and Logic Programming, volume 5, pages 499–590. Oxford University Press, 1998.Google Scholar
  33. 33.
    G. Nadathur and D. Mitchell. System description: Teyjus-a compiler and abstract machine based implementation of λProlog. In Automated Deduction-CADE-13, Springer-Verlag LNAI no. 1632, pages 287–291, July 1999.Google Scholar
  34. 34.
    R. Paul. Sparc architecture, assembly language programming, and C. Prentice Hall, second edition, 2000.Google Scholar
  35. 35.
    F. Pereira and D. Warren. Definite clause grammars for language analysis. Artificial Intelligence, 13:231–278, 1980.zbMATHCrossRefMathSciNetGoogle Scholar
  36. 36.
    F. Pereira and D. Warren. Parsing as deduction. In 21st Annual Meeting of the Association for Computational Linguistics, pages 137–144, 1983.Google Scholar
  37. 37.
    F. Pfenning. Logic programming in the LF logical framework. In G. Huet and G. D. Plotkin, editors, Logical Frameworks. Cambridge University Press, 1991.Google Scholar
  38. 38.
    F. Pfenning and C. Elliot. Higher-order abstract syntax. In ACM-SIGPLAN Conference on Programming Language Design and Implementation, pages 199–208. ACM Press, 1988.Google Scholar
  39. 39.
    A. Sabry and M. Felleisen. Reasoning about programs in continuation-passing style. Lisp and Symbolic Computation, 6(3/4):289–360, 1993.CrossRefGoogle Scholar
  40. 40.
    M. Wand. Correctness of procedure representations in higher-order assembly language. In Proceedings: Mathematical Foundations of Programming Semantics’ 91, pages 294–311. Springer-Verlag LNCS vol. 598, 1992.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2002

Authors and Affiliations

  • Chuck C. Liang
    • 1
  1. 1.Department of Computer ScienceHofstra UniversityHempstead, New YorkUSA

Personalised recommendations