Advertisement

Higher-Order Abstract Syntax with induction in Coq

  • Joëlle Despeyroux
  • André Hirschowitz
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 822)

Abstract

Three important properties of Higher-Order Abstract Syntax are the (higher-order) induction principle, which allows proofs by induction, the (higher-order) injection principle, which asserts that equal terms have equal heads and equal sons, and the extensionality principle, which asserts that functional terms which are pointwise equal are equal. Higher-order abstract syntax is implemented for instance in the Edinburgh Logical Framework and the above principles are satisfied by this implementation. But although they can be proved at the meta level, they cannot be proved at the object level and furthermore, it is not so easy to know how to formulate them in a simple way at the object level. We explain here how Second-Order Abstract Syntax can be implemented in a more powerful type system (Coq) in such a way as to make available or provable (at the object level) the corresponding induction, injection and extensionality principles.

Keywords

Abstract Syntax Object Level Extensionality Principle Inductive Type Induction Principle 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    A. Avron, F. Honsell, and A. Mason. Using typed λ-calculus to implement formal systems on a machine. Technical Report ECS-LFCS-87-31, Edinburgh University, July 1987.Google Scholar
  2. 2.
    Th. Despeyroux and A. Hirschowitz. A categorical approach to higher-order abstract syntax, forthcoming paper, 1994.Google Scholar
  3. 3.
    G. Dowek, A. Felty, H. Herbelin, G. Huet, C. Murthy, C. Parent, Ch. Paulin-Mohring, and B. Werner. The coq proof assistant user's guide, version 5.8. Technical Report 154, Inria, Rocquencourt, France, May 1993.Google Scholar
  4. 4.
    C. Elliot and F. Pfenning. Higher-order abstract syntax. In Proceedings of the ACM SIGPLAN' 88 International Conference on Programming Language Design and Implementation, Atlanta, Georgia, USA, June 22–24, 1988.Google Scholar
  5. 5.
    J. Hannan and D. Miller. Enriching a meta-language with higher-order features. In Proceedings of the Workshop on Meta-Programming in Logic Programming, Bristol, June 1988.Google Scholar
  6. 6.
    J. Hannan and F. Pfenning. Compiler verification in LF. In IEEE, editor, Proceedings of the LICS International Conference on Logic In Computer Sciences, Santa Cruz, California, June 1992.Google Scholar
  7. 7.
    R. Harper. Systems of polymorphic type assignment in LF. Technical Report CMU-CS-90-144, Carnegie Mellon University, Pittsburgh, Pennsylvania, June 1990.Google Scholar
  8. 8.
    R. Harper, F. Honsell, and G. Plotkin. A framework for defining logics. In IEEE, editor, Proceedings of the second LICS International Conference on Logic In Computer Sciences, Cornell, USA, pages 194–204, 1987.Google Scholar
  9. 9.
    R. Harper, F. Honsell, and G. Plotkin. A framework for defining logics. Technical Report ECS-LFCS-91-162, Edinburgh University, June 1991.Google Scholar
  10. 10.
    G. Huet. Constructive computation theory. part I. Lecture notes. October 1992.Google Scholar
  11. 11.
    G. Kahn. Natural semantics. In Proceedings of the Symp. on Theorical Aspects of Computer Science, Passau, Germany, 1987. also available as a Research Report RR-601, Inria, Sophia-Antipolis, February 1987.Google Scholar
  12. 12.
    S. Michaylov and F. Pfenning. Natural semantics and some of its meta-theory in elf. In Lars Halln"as, editor, Proceedings of the Second Workshop on Extentions of Logic Programing, Springer-Verlag LNCS, 1991. also available as a Technical Report MPI-I-91-211, Max-Planck-Institute for Computer Science,Saarbrucken, Germany, August 1991.Google Scholar
  13. 13.
    D. Miller and G. Nadathur. An overview of λ-prolog. In MIT Press, editor, Proceedings of the International Logic Programming Conference, Seattle, Washington, pages 910–827, August 1988.Google Scholar
  14. 14.
    Ch. Paulin-Mohring. Inductive definitions in the system coq. rules and properties. In J.F. Groote M. Bezem, editor, Proceedings of the International Conference on Typed Lambda Calculi and Applications, TLCA'93, Springer-Verlag LNCS 664, pages 328–345, 1992. also available as a Research Report RR-92-49, Dec. 1992, ENS Lyon, France.Google Scholar
  15. 15.
    L. C. Paulson. The foundation of a generic theorem prover. Journal of Automated Reasoning, 5:363–397, 1989.Google Scholar
  16. 16.
    F. Pfenning. Elf: A language for logic definition and verified metaprogramming. In Proceedings of the fourth ACM-IEEE Symp. on Logic In Computer Science, Asilomar, California, USA, June 1989.Google Scholar
  17. 17.
    F. Pfenning and E. Rohwedder. Implementing the meta-theory of deductive systems. In Proceedings of the CADE-11 Conference, 1991.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1994

Authors and Affiliations

  • Joëlle Despeyroux
    • 1
  • André Hirschowitz
    • 2
  1. 1.INRIA-Sophia-AntipolisSophia-Antipolis CedexFrance
  2. 2.CNRS URA 168University of NiceNice Cedex 2France

Personalised recommendations