Skip to main content
SpringerLink
Log in

Abstract Syntax for Variable Binders: An Overview

  • Conference paper
  • First Online:
Computational Logic — CL 2000 (CL 2000)

Part of the book series: Lecture Notes in Computer Science ((LNAI,volume 1861))

Included in the following conference series:

Abstract

A large variety of computing systems, such as compilers, interpreters, static analyzers, and theorem provers, need to manipulate syntactic objects like programs, types, formulas, and proofs. A common characteristic of these syntactic objects is that they contain variable binders, such as quantifiers, formal parameters, and blocks. It is a common observation that representing such binders using only first-order expressions is problematic since the notions of bound variable names, free and bound occurrences, equality up to alpha-conversion, substitution, etc., are not addressed naturally by the structure of first-order terms (labeled trees). This overview describes a higher-level and more declarative approach to representing syntax within such computational systems. In particular, we shall focus on a representation of syntax called higher-order abstract syntax and on a more primitive version of that representation called λ-tree syntax.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Martin Abadi, Luca Cardelli, Pierre-Louis Curien, and Jean-Jacques Lévy. Explicit substitutions. Journal of Functional Programming, 1(4):375–416, October 1991.

    Google Scholar 

  2. N. de Bruijn. Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser Theorem. Indag. Math., 34(5):381–392, 1972.

    Google Scholar 

  3. Alonzo Church. A formulation of the simple theory of types. Journal of Symbolic Logic, 5:56–68, 1940.

    Article  MATH  MathSciNet  Google Scholar 

  4. Joelle Despeyroux, Amy Felty, and Andre Hirschowitz. Higher-order abstract syntax in Coq. In Second International Conference on Typed Lambda Calculi and Applications, pages 124–138, April 1995.

    Google Scholar 

  5. Joelle Despeyroux and Andre Hirschowitz. Higher-order abstract syntax with induction in Coq. In Fifth International Conference on Logic Programming and Automated Reasoning, pages 159–173, June 1994.

    Google Scholar 

  6. Joelle Despeyroux, Frank Pfenning, and Carsten Schürmann. Primitive recursion for higher-order abstract syntax. In Third International Conference on Typed Lambda Calculi and Applications, April 1997.

    Google Scholar 

  7. G. Dowek, T. Hardin, and C. Kirchner. Higher-order unification via explicit substitutions. In D. Kozen, editor, Logic in Computer Science, pages 366–374, 1995.

    Google Scholar 

  8. M. P. Fiore, G. D. Plotkin, and D. Turi. Abstract syntax and variable binding. In Logic in Computer Science, pages 193–202. IEEE Computer Society Press, 1999.

    Google Scholar 

  9. M. J. Gabbay and A. M. Pitts. A new approach to abstract syntax involving binders. In Logic in Computer Science, pages 214–224. IEEE Computer Society Press, 1999.

    Google Scholar 

  10. Robert Harper, Furio Honsell, and Gordon Plotkin. A framework for defining logics. Journal of the ACM, 40(1):143–184, 1993.

    Article  MATH  MathSciNet  Google Scholar 

  11. M. Hofmann. Semantical analysis of higher-order abstract syntax. In Logic in Computer Science, pages 204–213. IEEE Computer Society Press, 1999.

    Google Scholar 

  12. Gérard Huet. A unification algorithm for typed λ-calculus. Theoretical Computer Science, 1:27–57, 1975.

    Article  MathSciNet  Google Scholar 

  13. Gérard Huet and Bernard Lang. Proving and applying program transformations expressed with second-order patterns. Acta Informatica, 11:31–55, 1978.

    Article  MATH  MathSciNet  Google Scholar 

  14. Dale Miller. An extension to ML to handle bound variables in data structures: Preliminary report. In Informal Proceedings of the Logical Frameworks BRA Workshop, June 1990. Available as UPenn CIS technical report MS-CIS-90-59.

    Google Scholar 

  15. Dale Miller. A logic programming language with lambda-abstraction, function variables, and simple unification. J. of Logic and Computation, 1(4):497–536, 1991.

    Article  MATH  Google Scholar 

  16. Dale Miller. Unification of simply typed lambda-terms as logic programming. In Eighth International Logic Programming Conference, pages 255–269, Paris, France, June 1991. MIT Press.

    Google Scholar 

  17. Dale Miller. Abstract syntax and logic programming. In Logic Programming: Proceedings of the First and Second Russian Conferences on Logic Programming, number 592 in LNAI, pages 322–337. Springer-Verlag, 1992.

    Google Scholar 

  18. Dale Miller. Unification under a mixed prefix. Journal of Symbolic Computation, pages 321–358, 1992.

    Google Scholar 

  19. Dale Miller and Gopalan Nadathur. Higher-order logic programming. In Ehud Shapiro, editor, Proceedings of the Third International Logic Programming Conference, pages 448–462, London, June 1986.

    Google Scholar 

  20. Dale Miller and Gopalan Nadathur. Some uses of higher-order logic in computational linguistics. In Proceedings of the 24th Annual Meeting of the Association for Computational Linguistics, pages 247–255, 1986.

    Google Scholar 

  21. Dale Miller and Gopalan Nadathur. A logic programming approach to manipulating formulas and programs. In Seif Haridi, editor, IEEE Symposium on Logic Programming, pages 379–388, San Francisco, September 1987.

    Google Scholar 

  22. Dale Miller, Gopalan Nadathur, Frank Pfenning, and Andre Scedrov. Uniform proofs as a foundation for logic programming. Annals of Pure and Applied Logic, 51:125–157, 1991.

    Article  MathSciNet  MATH  Google Scholar 

  23. Dale Miller and Catuscia Palamidessi. Foundational aspects of syntax. In Pierpaolo Degano, Roberto Gorrieri, Alberto Marchetti-Spaccamela, and Peter Wegner, editors, ACM Computing Surveys Symposium on Theoretical Computer Science: A Perspective, volume 31. ACM, Sep 1999. Article number 10.

    Google Scholar 

  24. John C. Mitchell and Eugenio Moggi. Kripke-style models for typed lambda calculus. Annals of Pure and Applied Logic, 51, 1991.

    Google Scholar 

  25. Gopalan Nadathur. A fine-grained notation for lambda terms and its use in intensional operations. Journal of Functional and Logic Programming, 1999(2), March 1999.

    Google Scholar 

  26. Gopalan Nadathur and Dale Miller. An Overview of λProlog. In Fifth International Logic Programming Conference, pages 810–827, Seattle, Washington, August 1988. MIT Press.

    Google Scholar 

  27. Gopalan Nadathur and Dustin J. Mitchell. System description: Teyjus—a compiler and abstract machine based implementation of λProlog. In H. Ganzinger, editor, CADE-16, pages 287–291, Trento, Italy, July 1999. Springer LNCS.

    Google Scholar 

  28. Gopalan Nadathur and Debra Sue Wilson. A notation for lambda terms: A generalization of environments. Theoretical Computer Science, 198(1–2):49–98, 1998.

    Article  MATH  MathSciNet  Google Scholar 

  29. Tobias Nipkow. Higher-order critical pairs. In G. Kahn, editor, Sixth Annual Sym. on Logic in Computer Science, pages 342–349. IEEE, July 1991.

    Google Scholar 

  30. Tobias Nipkow. Functional unification of higher-order patterns. In M. Vardi, editor, Eighth Annual Sym. on Logic in Computer Science, pages 64–74. IEEE, June 1993.

    Google Scholar 

  31. Lawrence C. Paulson. The foundation of a generic theorem prover. Journal of Automated Reasoning, 5:363–397, September 1989.

    Google Scholar 

  32. Lawrence C. Paulson. Isabelle: The next 700 theorem provers. In Piergiorgio Odifreddi, editor, Logic and Computer Science, pages 361–386. Academic Press, 1990.

    Google Scholar 

  33. Frank Pfenning. Elf: A language for logic definition and verified metaprogramming. In Fourth Annual Symposium on Logic in Computer Science, pages 313–321, Monterey, CA, June 1989.

    Google Scholar 

  34. Frank Pfenning. Unification and anti-unification in the Calculus of Constructions. In G. Kahn, editor, Sixth Annual Symposium on Logic in Computer Science, pages 74–85. IEEE, July 1991.

    Google Scholar 

  35. Frank Pfenning. The practice of logical frameworks. In Héléne Kirchner, editor, Proceedings of the Colloquium on Trees in Algebra and Programming, volume LNCS 1059, pages 119–134. Springer-Verlag, 1996.

    Google Scholar 

  36. Frank Pfenning and Conal Elliot. Higher-order abstract syntax. In Proceedings of the ACM-SIGPLAN Conference on Programming Language Design and Implementation, pages 199–208. ACM Press, June 1988.

    Google Scholar 

  37. Andrew M. Pitts and Murdoch J. Gabbay. A meta language for programming with bound names modulo renaming (preliminary report). Draft January 2000.

    Google Scholar 

  38. Zhenyu Qian. Unification of higher-order patterns in linear time and space. J. Logic and Computation, 6(3):315–341, 1996.

    Article  MATH  MathSciNet  Google Scholar 

  39. Richard Statman. The typed λ calculus is not elementary recursive. Theoretical Computer Science, 9:73–81, 1979.

    Article  MATH  MathSciNet  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computer Science and Engineering 220 Pond Laboratory, The Pennsylvania State University, University Park, PA, 16802-6106, USA

    Dale Miller

Authors
  1. Dale Miller
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. The Australian National University, Australia

    John Lloyd

  2. Simon Fraser University, Canada

    Veronica Dahl

  3. Universität Koblenz, Germany

    Ulrich Furbach

  4. The University of Birmingham, UK

    Manfred Kerber

  5. University of Manchester, UK

    Kung-Kiu Lau

  6. The Pennsylvania State University, USA

    Catuscia Palamidessi

  7. Universidade Nova de Lisboa, Portugal

    Luís Moniz Pereira

  8. The Hebrew University of Jerusalem, Israel

    Yehoshua Sagiv

  9. The University of Melbourne, Australia

    Peter J. Stuckey

Rights and permissions

Reprints and permissions

Copyright information

© 2000 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Miller, D. (2000). Abstract Syntax for Variable Binders: An Overview. In: Lloyd, J., et al. Computational Logic — CL 2000. CL 2000. Lecture Notes in Computer Science(), vol 1861. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-44957-4_16

Download citation

  • DOI: https://doi.org/10.1007/3-540-44957-4_16

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-67797-0

  • Online ISBN: 978-3-540-44957-7

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation