Skip to main content
SpringerLink
Log in
Book cover

International Conference on Theorem Proving in Higher Order Logics

TPHOLs 2003: Theorem Proving in Higher Order Logics pp 238–252Cite as

Extending Higher-Order Unification to Support Proof Irrelevance

  • Conference paper

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 2758))

Abstract

As theories and proofs in logical frameworks become larger, careful control over what information within them can safely be omitted or erased becomes useful for efficient implementation. The notion of proof irrelevance provides exactly this control, but requires existing algorithms used in logical frameworks, in particular higher-order pattern unification, to be extended to accommodate the richer type theory. We describe this extended algorithm, whose presentation is simplified by making use of recent developments in explaining unification metavariables as modal variables, which obviates the need for full explicit substitutions.

This work has been partially supported by NSF Grant CCR-9988281 “Logical and Meta-Logical Frameworks”. Thanks are owed to Frank Pfenning, Brigitte Pientka, Kaustuv Chaudhuri, and the anonymous reviewers for many useful comments and corrections.

This is a preview of subscription content, 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

Learn about institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Abadi, M., Cardelli, L., Curien, P.-L., Lèvy, J.-J.: Explicit substitutions. In: Conference Record of the Seventeenth Annual ACM Symposium on Principles of Programming Languages, San Francisco, California, pp. 31–46. ACM Press, New York (1990)

    Google Scholar 

  2. Crary, K., Sarkar, S.: A metalogical approach to foundational certified code. Technical Report CMU-CS-03-108, Carnegie Mellon University (January 2003)

    Google Scholar 

  3. Dowek, G., Hardin, T., Kirchner, C.: Higher-order unification via explicit substitutions. In: Kozen, D. (ed.) Proceedings of the Tenth Annual Symposium on Logic in Computer Science, San Diego, California, June 1995, pp. 366–374. IEEE Computer Society Press, Los Alamitos (1995)

    Chapter  Google Scholar 

  4. Dowek, G., Hardin, T., Kirchner, C., Pfenning, F.: Unification via explicit substitutions: The case of higher-order patterns. In: Maher, M. (ed.) Proceedings of the Joint International Conference and Symposium on Logic Programming, Bonn, Germany, September 1996, pp. 259–273. MIT Press, Cambridge (1996)

    Google Scholar 

  5. Harper, R., Honsell, F., Plotkin, G.: A framework for defining logics. Journal of the Association for Computing Machinery 40(1), 143–184 (1993)

    MATH  MathSciNet  Google Scholar 

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

    Article  MATH  MathSciNet  Google Scholar 

  7. Pfenning, F.: Intensionality, extensionality, and proof irrelevance in modal type theory. In: Halpern, J. (ed.) Proceedings of the 16th Annual Symposium on Logic in Computer Science (LICS 2001), Boston, Massachusetts, June 2001, pp. 221–230. IEEE Computer Society Press, Los Alamitos (2001)

    Chapter  Google Scholar 

  8. Pfenning, F., Elliott, C.: Higher-order abstract syntax. In: Proceedings of the ACM SIGPLAN 1988 Symposium on Language Design and Implementation, Atlanta, Georgia, June 1998, pp. 199–208 (1998)

    Google Scholar 

  9. Pientka, B., Pfenning, F.: Optimizing higher-order pattern unification. In: Baader, F. (ed.) CADE 2003. LNCS (LNAI), vol. 2741, pp. 473–487. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  10. Reed, J.: Higher-order pattern unification and proof irrelevance. Appears in TPHOLs 2002 Track B proceedings, NASA tech report CP-2002-211736 (2002)

    Google Scholar 

  11. Reed, J.: Proof irrelevance and strict definitions in a logical framework. Technical Report CMU-CS-02-153, Carnegie Mellon University (2002)

    Google Scholar 

  12. Rohwedder, E., Pfenning, F.: Mode and termination checking for higher-order logic programs. In: Riis Nielson, H. (ed.) ESOP 1996. LNCS, vol. 1058, pp. 296–310. Springer, Heidelberg (1996)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Carnegie Mellon University, PA, 15213, USA, Pittsburgh

    Jason Reed

Authors
  1. Jason Reed
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Information Security Group, Dep. of Computer Science, ETH Zurich, Switzerland

    David Basin

  2. Computer Science Dept., Saarland University, 66123, Saarbrücken, Germany

    Burkhart Wolff

Rights and permissions

Reprints and permissions

Copyright information

© 2003 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Reed, J. (2003). Extending Higher-Order Unification to Support Proof Irrelevance. In: Basin, D., Wolff, B. (eds) Theorem Proving in Higher Order Logics. TPHOLs 2003. Lecture Notes in Computer Science, vol 2758. Springer, Berlin, Heidelberg. https://doi.org/10.1007/10930755_16

Download citation

  • DOI: https://doi.org/10.1007/10930755_16

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-40664-8

  • Online ISBN: 978-3-540-45130-3

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation