Skip to main content
SpringerLink
Log in

Combining de Bruijn Indices and Higher-Order Abstract Syntax in Coq

  • Conference paper
Types for Proofs and Programs (TYPES 2006)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 4502))

Included in the following conference series:

Abstract

The use of higher-order abstract syntax is an important approach for the representation of binding constructs in encodings of languages and logics in a logical framework. Formal meta-reasoning about such object languages is a particular challenge. We present a mechanism for such reasoning, formalized in Coq, inspired by the Hybrid tool in Isabelle. At the base level, we define a de Bruijn representation of terms with basic operations and a reasoning framework. At a higher level, we can represent languages and reason about them using higher-order syntax. We take advantage of Coq’s constructive logic by formulating many definitions as Coq programs. We illustrate the method on two examples: the untyped lambda calculus and quantified propositional logic. For each language, we can define recursion and induction principles that work directly on the higher-order 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. Ambler, S.J., Crole, R.L., Momigliano, A.: Combining higher order abstract syntax with tactical theorem proving and (co)induction. In: Carreño, V.A., Muñoz, C.A., Tahar, S. (eds.) TPHOLs 2002. LNCS, vol. 2410, pp. 13–30. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  2. Aydemir, B.E., Bohannon, A., Fairbairn, M., Foster, J.N., Pierce, B.C., Sewell, P., Vytiniotis, D., Washburn, G., Weirich, S., Zdancewic, S.: Mechanized metatheory for the masses: The POPLmark challenge. In: RSCTC 2000. LNCS, pp. 50–65. Springer, Heidelberg (2005), http://fling-l.seas.upenn.edu/~plclub/cgi-bin/poplmark/index.php?title=The_POPLmark_Challenge

    Google Scholar 

  3. Bertot, Y., Castéran, P.: Interactive Theorem Proving and Program Development. Coq’Art: The Calculus of Inductive Constructions. Springer, Heidelberg (2004)

    MATH  Google Scholar 

  4. Coq Development Team, LogiCal Project. The Coq Proof Assistant reference manual: Version 8.0. Technical report, INRIA (2006)

    Google Scholar 

  5. Coquand, T., Huet, G.: The Calculus of Constructions. Information and Computation 76, 95–120 (1988)

    Article  MATH  MathSciNet  Google Scholar 

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

    Google Scholar 

  7. Despeyroux, J., Felty, A., Hirschowitz, A.: Higher-order abstract syntax in Coq. In: Dezani-Ciancaglini, M., Plotkin, G. (eds.) TLCA 1995. LNCS, vol. 902, pp. 124–138. Springer, Heidelberg (1995)

    Chapter  Google Scholar 

  8. Felty, A.P.: Two-level meta-reasoning in Coq. In: Carreño, V.A., Muñoz, C.A., Tahar, S. (eds.) TPHOLs 2002. LNCS, vol. 2410, pp. 198–213. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  9. Gabbay, M.J., Pitts, A.M.: A new approach to abstract syntax with variable binding. Formal Aspects of Computing 13, 341–363 (2001)

    Article  Google Scholar 

  10. Gordon, A.D.: A mechanisation of name-carrying syntax up to alpha-conversion. In: Sixth International Workshop on Higher-Order Logic Theorem Proving and its Applications. LNCS, pp. 413–425. Springer, Heidelberg (1993)

    Google Scholar 

  11. Gordon, A.D., Melham, T.: Five axioms of alpha-conversion. In: Lanzi, P.L., Stolzmann, W., Wilson, S.W. (eds.) IWLCS 2000. LNCS (LNAI), vol. 1996, pp. 173–190. Springer, Heidelberg (2001)

    Google Scholar 

  12. McDowell, R., Miller, D.: Reasoning with higher-order abstract syntax in a logical framework. ACM Transactions on Computational Logic 3(1), 80–136 (2002)

    Article  MathSciNet  Google Scholar 

  13. Melham, T.F.: A mechanized theory of the Π-calculus in HOL. Nordic Journal of Computing 1(1), 50–76 (1994)

    MathSciNet  Google Scholar 

  14. Miculan, M.: Developing (meta)theory of λ-calculus in the theory of contexts. Electronic Notes in Theoretical Computer Science 58(1), 37–58 (2001) (MERLIN 2001: Mechanized Reasoning about Languages with Variable Binding)

    Article  MathSciNet  Google Scholar 

  15. Miculan, M.: On the formalization of the modal μ-calculus in the calculus of inductive constructions. Information and Computation 164(1), 199–231 (2001)

    Article  MATH  MathSciNet  Google Scholar 

  16. Miller, D., Tiu, A.: A proof theory for generic judgments. ACM Transactions on Computational Logic 6(4), 749–783 (2005)

    Article  MathSciNet  Google Scholar 

  17. Momigliano, A., Ambler, S.J.: Multi-level meta-reasoning with higher-order abstract syntax. In: Sixth International Conference on Foundations of Software Science and Computational Structures, April 2003. LNCS, pp. 375–391. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  18. Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle/HOL — A Proof Assistant for Higher-Order Logic. LNCS. Springer, Heidelberg (2002)

    MATH  Google Scholar 

  19. Nogin, A., Kopylov, A., Yu, X., Hickey, J.: A computational approach to reflective meta-reasoning about languages with bindings. In: MERLIN 2005. Proceedings of the 3rd ACM SIGPLAN Workshop on MEchanized Reasoning about Languages with varIable biNding, pp. 2–12. ACM Press, New York (2005)

    Chapter  Google Scholar 

  20. Norrish, M.: Recursive function definition for types with binders. In: Slind, K., Bunker, A., Gopalakrishnan, G.C. (eds.) TPHOLs 2004. LNCS, vol. 3223, pp. 241–256. Springer, Heidelberg (2004)

    Google Scholar 

  21. Pfenning, F., Schürmann, C.: System description: Twelf — a meta-logical framework for deductive systems. In: Ganzinger, H. (ed.) Automated Deduction - CADE-16. LNCS (LNAI), vol. 1632, pp. 202–206. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  22. Pollack, R.: Reasoning about languages with binding. Presentation (2006), available at http://homepages.inf.ed.ac.uk/rap/export/bindingChallenge_slides.pdf

  23. Schürmann, C.: Automating the Meta Theory of Deductive Systems. PhD thesis, Carnegie Mellon University (2000)

    Google Scholar 

  24. Schürmann, C., Despeyroux, J., Pfenning, F.: Primitive recursion for higher-order abstract syntax. Theoretical Computer Science 266, 1–57 (2001)

    Article  MATH  MathSciNet  Google Scholar 

  25. Schürmann, C., Poswolsky, A., Sarnat, J.: The ∇-calculus. Functional programming with higher-order encodings. In: Urzyczyn, P. (ed.) TLCA 2005. LNCS, vol. 3461, pp. 339–353. Springer, Heidelberg (2005)

    Google Scholar 

  26. Stump, A.: POPLmark 1a with named bound variables. Presented at the Progress on Poplmark Workshop (January 2006)

    Google Scholar 

  27. Werner, B.: Méta-théorie du Calcul des Constructions Inductives. PhD thesis, Université Paris 7 (1994)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. School of Information Technology and Engineering, and Department of Mathematics and Statistics, University of Ottawa, Canada

    Venanzio Capretta & Amy P. Felty

Authors
  1. Venanzio Capretta
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Amy P. Felty
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Thorsten Altenkirch Conor McBride

Rights and permissions

Reprints and permissions

Copyright information

© 2007 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Capretta, V., Felty, A.P. (2007). Combining de Bruijn Indices and Higher-Order Abstract Syntax in Coq. In: Altenkirch, T., McBride, C. (eds) Types for Proofs and Programs. TYPES 2006. Lecture Notes in Computer Science, vol 4502. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-74464-1_5

Download citation

  • DOI: https://doi.org/10.1007/978-3-540-74464-1_5

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-74463-4

  • Online ISBN: 978-3-540-74464-1

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation