F. Pfenning
ABSTRACT
We describe motivation, design, use, and implementation of higher-order abstract syntax as a central representation for programs, formulas, rules, and other syntactic objects in program manipulation and other formal systems where matching and substitution or unification are central operations. Higher-order abstract syntax incorporates name binding information in a uniform and language generic way. Thus it acts as a powerful link integrating diverse tools in such formal environments. We have implemented higher-order abstract syntax, a supporting matching and unification algorithm, and some clients in Common Lisp in the framework of the Ergo project at Carnegie Mellon University.
- 1.Amon Avron, Furio A. Honsell, and Ian A. Mason. Using typed Lambda Calculus to Implement Formal Systems on a Machine. Technical Report ECS- LFCS-87-31, Laboratory for Foundations of Computer Science, University of Edinburgh, Edinburgh, Scotland, June 1987.Google Scholar
- 2.Roff Bahlke and Gregor Snelting. The PSG system: from formal language definitions to interactive programming environments. ACM Transactions on Programming Languages and Systems, 8(4):547- 576, October 1986. Google ScholarDigital Library
- 3.R. M. Burstall and John Darlington. A transformation system for developing recursive programs. Journal of the Association for Computing Machinery, 24(1):44-67, January 1977. Google ScholarDigital Library
- 4.Alonzo Church. A formulation of the simple theory Of types. Journal of Symbolic Logic, 5:56--68, 1940.Google ScholarCross Ref
- 5.N. G. de Bruijn. Lambda-calculus notation with nameless dummies: a tool for automatic formula manipulation with application to the Church-Rosser theorem, lndag. Math., 34(5):381-392, 1972.Google Scholar
- 6.David Garlan. Views for Tools in Integrated Environments. PhD thesis, Carnegie Mellon University, 1987. Available as Technical Report CMU-CS-87- 147. Google ScholarDigital Library
- 7.Timothy G. Griffin. An Environment for Formal Systems. Technical Report 87-846, Department of Computer Science, Cornell University, Ithaca, New York, June 1987. Google ScholarDigital Library
- 8.Gandalf Group. Special issue on the Gandalf project. In The Journal of Systems and Software, Volume 5, Number 2, May 1985.Google Scholar
- 9.Robert Harper, Furio Honsell, and Gordon Plotkin. A framework for defining logics. In Symposium on Logic in Computer Science, pages 194-204, IEEE, June 1987.Google Scholar
- 10.G6rard Huet. A unification algorithm for typed )~- calculus. Theoretical Computer Science, 1:27-57, 1975.Google ScholarCross Ref
- 11.G6rard Huet and Bernard Lang. Proving and applying program transformations expressed with second-order patterns. Acta lnformatica, 11:31-55, 1978.Google Scholar
- 12.Dale Miller, Gopalan Naclathur, and Andre Scedrov. Hereditary Harrop formulas and uniform proof systems. In Second Annual Symposium on Logic in Computer Science, pages 98-105, IEEE, June 1987.Google Scholar
- 13.Dale A. Miller. Unification under mixed prefixes. 1987. Unpublished manuscript.Google Scholar
- 14.Dale A. Miller and Gopalan Nadathur. Higher-order logic programming. In Procee&'ngs of the Third International Conference on Logic Programming, Springer Verlag, July 1986. Google ScholarDigital Library
- 15.Dale A. Miller and Gopalan Nadathur. A logic programming approach to manipulating formulas and programs. In Symposium on Logic Programming, San Francisco, IEEE, September 1987.Google Scholar
- 16.B. M/511er. A survey of the project CIP: Computeraided, intuition-guided programming. Technical Report TUM-18406, Institut fur Informatik tier TU MUnchen, Munich, West Germany, 1984.Google Scholar
- 17.Gopalan Naclathur. A Higher-Order Logic as the Basis for Logic Programming. PhD thesis, University of Pennsylvania, 1987. Google ScholarDigital Library
- 18.Lawrence Paulson. Natural deduction as higherorder resolution. Journal of Logic Programming, 3:237-258, 1986. Google ScholarDigital Library
- 19.Thomas Reps and Tim Teitelbaum. The synthesizer generator. In Proceedings of the A CM SIG- SOFT/SIGPLAN Software Engineering Symposium on Practical Software Development Environments, pages 42--48, ACM, New York, April 1984. Google ScholarDigital Library
- 20.David S. Wile. POPART: Producer of Parsers and Related Tools, System Builder's Manual. Technical Report, University of Southern California, Information Sciences Institute, 1987.Google Scholar
Index Terms
- Higher-order abstract syntax
Recommendations
Parametric higher-order abstract syntax for mechanized semantics
ICFP '08: Proceedings of the 13th ACM SIGPLAN international conference on Functional programmingWe present parametric higher-order abstract syntax (PHOAS), a new approach to formalizing the syntax of programming languages in computer proof assistants based on type theory. Like higher-order abstract syntax (HOAS), PHOAS uses the meta language's ...
Higher-order abstract syntax in classical higher-order logic
LFMTP '09: Proceedings of the Fourth International Workshop on Logical Frameworks and Meta-Languages: Theory and PracticeHigher-Order Abstract Syntax, or HOAS, is a technique for using a higher-order logic as a metalanguage for an object language with binding operators. It avoids formalizing syntactic details related to variable binding. This paper gives an extension to ...
Reasoning with higher-order abstract syntax in a logical framework
Logical frameworks based on intuitionistic or linear logics with higher-type quantification have been successfully used to give high-level, modular, and formal specifications of many important judgments in the area of programming languages and inference ...
Comments