Skip to main content
SpringerLink
Log in
Book cover

International Conference on Theorem Proving in Higher Order Logics

TPHOLs 2004: Theorem Proving in Higher Order Logics pp 18–33Cite as

Verifying Uniqueness in a Logical Framework

  • Conference paper

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

Abstract

We present an algorithm for verifying that some specified arguments of an inductively defined relation in a dependently typed λ-calculus are uniquely determined by some other arguments. We prove it correct and also show how to exploit this uniqueness information in coverage checking, which allows us to verify that a definition of a function or relation covers all possible cases. In combination, the two algorithms significantly extend the power of the meta-reasoning facilities of the Twelf implementation of LF.

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. Coquand, T.: An algorithm for testing conversion in type theory. In: Huet, G., Plotkin, G. (eds.) Logical Frameworks, pp. 255–279. Cambridge University Press, Cambridge (1991)

    Chapter  Google Scholar 

  2. Coquand, T.: Pattern matching with dependent types. In: Proceedings of the Workshop on Types for Proofs and Programs, Båstad, Sweden, pp. 71–83 (1992)

    Google Scholar 

  3. Crary, K.: Toward a foundational typed assembly language. In: Morrisett, G. (ed.) Proceedings of the 30th Annual Symposium on Principles of Programming Languages, New Orleans, Louisiana, January 2003, pp. 198–212. ACM Press, New York (2003)

    Google Scholar 

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

    Google Scholar 

  5. Despeyroux, J., Leleu, P.: A modal lambda calculus with iteration and case constructs. In: Altenkirch, T., Naraschewski, W., Reus, B. (eds.) TYPES 1998. LNCS, vol. 1657, pp. 47–61. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  6. 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 

  7. 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 

  8. Harper, R., Pfenning, F.: On equivalence and canonical forms in the LF type theory. Transactions on Computational Logic (2003); To appear. Preliminary version available as Technical Report CMU-CS-00-148

    Google Scholar 

  9. Hofmann, M.: Extensional Concepts in Intensional Type Theory. PhD thesis, Department of Computer Science, University of Edinburgh (July 1995); available as Technical Report CST-117-95

    Google Scholar 

  10. Hofmann, M., Streicher, T.: The groupoid model refutes uniqueness of identity proofs. In: Proceedings of the 9th Annual Symposium on Logic in Computer Science (LICS 1994), Paris, France, pp. 208–212. IEEE Computer Society Press, Los Alamitos (1994)

    Chapter  Google Scholar 

  11. McBride, C.: Dependently Typed Functional Programs and their Proofs. PhD thesis, University of Edinburgh (1999); available as Technical Report ECS-LFCS-00-419.

    Google Scholar 

  12. Pfenning, F.: Structural cut elimination I. intuitionistic and classical logic. Information and Computation 157(1/2), 84–141 (2000)

    Article  MATH  MathSciNet  Google Scholar 

  13. Pfenning, F.: Logical frameworks. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, ch. 17, pp. 1063–1147. Elsevier Science and MIT Press (2001)

    Google Scholar 

  14. Pfenning, F., Schürmann, C.: Algorithms for equality and unification in the presence of notational definitions. In: Altenkirch, T., Naraschewski, W., Reus, B. (eds.) TYPES 1998. LNCS, vol. 1657, pp. 179–193. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

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

    Chapter  Google Scholar 

  16. Pientka, B.: Termination and reduction checking for higher-order logic programs. In: Goré, R.P., Leitsch, A., Nipkow, T. (eds.) IJCAR 2001. LNCS (LNAI), vol. 2083, pp. 401–415. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  17. Poswolsky, A., Schürmann, C.: Factoring pure logic programs. Draft manuscript (November 2003)

    Google Scholar 

  18. 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 

  19. Schürmann, C.: Automating the Meta Theory of Deductive Systems. PhD thesis, Department of Computer Science, Carnegie Mellon University (August 2000); Available as Technical Report CMU-CS-00-146

    Google Scholar 

  20. Schürmann, C.: Recursion for higher-order encodings. In: Fribourg, L. (ed.) CSL 2001. LNCS, vol. 2142, pp. 585–599. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  21. Schürmann, C.: A type-theoretic approach to induction with higher-order encodings. In: Nieuwenhuis, R., Voronkov, A. (eds.) LPAR 2001. LNCS (LNAI), vol. 2250, pp. 266–281. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  22. Schürmann, C.: Delphin – toward functional programming with logical frameworks. Technical Report TR #1272, Yale University, Department of Computer Science (2004)

    Google Scholar 

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

    Article  MATH  MathSciNet  Google Scholar 

  24. Schürmann, C., Pfenning, F.: A coverage checking algorithm for LF. In: Basin, D., Wolff, B. (eds.) TPHOLs 2003. LNCS, vol. 2758, pp. 120–135. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  25. Washburn, G., Weirich, S.: Boxes go bananas: Encoding higher-order abstract syntax with parametric polymorphism. In: Proceedings of the Eighth International Conference on Functional Programming, Uppsala, Sweden, August 2003, pp. 249–262. ACM Press, New York (2003)

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computer Science, Lafayette College,  

    Penny Anderson

  2. Department of Computer Science, Carnegie Mellon University,  

    Frank Pfenning

Authors
  1. Penny Anderson
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Frank Pfenning
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. School of Computing, University of Utah,  

    Konrad Slind

  2. Electrical and Computer Engineering Department, Utah State University, 4120 Old Main Hill, 84341, Logan, UT, USA

    Annette Bunker

  3. School of Computing, Univ. of Utah, 84112, Salt Lake City, UT, USA

    Ganesh Gopalakrishnan

Rights and permissions

Reprints and permissions

Copyright information

© 2004 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Anderson, P., Pfenning, F. (2004). Verifying Uniqueness in a Logical Framework. In: Slind, K., Bunker, A., Gopalakrishnan, G. (eds) Theorem Proving in Higher Order Logics. TPHOLs 2004. Lecture Notes in Computer Science, vol 3223. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-30142-4_2

Download citation

  • DOI: https://doi.org/10.1007/978-3-540-30142-4_2

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-23017-5

  • Online ISBN: 978-3-540-30142-4

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation