Skip to main content
SpringerLink
Log in
Book cover

International Workshop on Types for Proofs and Programs

TYPES 1998: Types for Proofs and Programs pp 179–193Cite as

Algorithms for Equality and Unification in the Presence of Notational Definitions

  • Conference paper
  • First Online:

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

Abstract

Notational definitions are pervasive in mathematical practice and are therefore supported in most automated theorem proving systems such as Coq [B+98], PVS [ORS92], Lego [LP92], or Isabelle [Pau94]. Semantically, notational definitions are transparent, that is, one obtains the meaning of an expression by interpreting the result of expanding all definitions. Pragmatically, however, expanding all definitions as they are encountered is unsatisfactory, since it can be computationally expensive and complicate the user interface.

This work was supported by NSF Grant CCR-9619584

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. Bruno Barras et al. The Coq Proof Assistant, Reference Manual, Version 6.2. INRIA, CNRS, France, 1998. 179

    Google Scholar 

  2. Iliano Cervesato and Frank Pfenning. A linear spine calculus. Technical Report CMU-CS-97-125, CMU, 1997. 180, 181

    Google Scholar 

  3. Gilles Dowek, Thérése Hardin, Claude Kirchner, and Frank Pfenning. Unification via explicit substitutions: The case of higher-order patterns. In Joint International Conference and Symposium on Logic Programming (JICSLP’ 96), Bonn, Germany, 1996. 189

    Google Scholar 

  4. Timothy G. Griffin. Notational definition — a formal account. In Third Annual Symposium on Logic in Computer Science, Edinburgh, Scotland, pages 372–383. IEEE, July 1988. 180

    Google Scholar 

  5. M. Hanus. The integration of functions into logic programming: From theory to practice. Journal of Logic Programming, 19&20:583–628, 1994. 180

    Article  MathSciNet  Google Scholar 

  6. Robert Harper, Furio Honsell, and Gordon Plotkin. A framework for defining logics. Journal of the Association for Computing Machinery, 40(1):143–184, January 1993. 179, 180, 181, 182, 183

    MATH  MathSciNet  Google Scholar 

  7. Chris Hankin and Daniel Le Métayer. Deriving algorithms from type inference systems: Application to strictness analysis. In Proceedings of the Twenty-First Annual ACM Symposium on Principles of Programming Languages, Portland, pages 202–212. ACM, January 1994. 188

    Google Scholar 

  8. Robert Harper and Frank Pfenning. A module system for a programming language based on the LF logical framework. Journal of Logic and Computation, 8(1):5–31, 1998. A preliminary version is available as Technical Report CMU-CS-92-191, September 1992. 183

    Article  MATH  MathSciNet  Google Scholar 

  9. Gérard Huet. A unification algorithm for typed λ-calculus. Theoretical Computer Science, 1:27–57, 1975. 180, 184

    Article  MathSciNet  Google Scholar 

  10. Zhaohui Luo and Robert Pollack. The LEGO proof development system: A user’s manual. Technical Report ECS-LFCS-92-211, University of Edinburgh, May 1992. 179

    Google Scholar 

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

    Article  MATH  MathSciNet  Google Scholar 

  12. S. Owre, J. M. Rushby, and N. Shankar. PVS: A prototype verification system. In Deepak Kapur, editor, 11th International Conference on Automated Deduction (CADE), volume 607 of Lecture Notes in Artificial Intelligence, pages 748–752, Saratoga, NY, June 1992. Springer-Verlag. 179

    Google Scholar 

  13. Lawrence C. Paulson. Isabelle: A Generic Theorem Prover. Springer-Verlag LNCS 828, 1994. 179

    MATH  Google Scholar 

  14. Frank Pfenning. Unification and anti-unification in the Calculus of Constructions. In Sixth Annual IEEE Symposium on Logic in Computer Science, pages 74–85, Amsterdam, The Netherlands, July 1991. 190

    Google Scholar 

  15. Frank Pfenning and Carsten Schürmann. Twelf User’s Guide, 1.2 edition, September 1998. Available as Technical Report CMU-CS-98-173, Carnegie Mellon University. 180, 188

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Carnegie Mellon University, School of Computer Science, Carnegie

    Frank Pfenning & Carsten Schürmann

Authors
  1. Frank Pfenning
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Carsten Schürmann
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Ludwig-Maximilians-Universität, Institut für Informatik, Oettingenstr. 67, D-80538, München, Germany

    Thorsten Altenkirch  & Bernhard Reus  & 

  2. Technische Universität München, Institut für Informatik, Arcisstr. 21-1528, D-80290, München, Germany

    Wolfgang Naraschewski

Rights and permissions

Reprints and permissions

Copyright information

© 1999 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Pfenning, F., Schürmann, C. (1999). Algorithms for Equality and Unification in the Presence of Notational Definitions. In: Altenkirch, T., Reus, B., Naraschewski, W. (eds) Types for Proofs and Programs. TYPES 1998. Lecture Notes in Computer Science, vol 1657. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-48167-2_13

Download citation

  • DOI: https://doi.org/10.1007/3-540-48167-2_13

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-66537-3

  • Online ISBN: 978-3-540-48167-6

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation