Skip to main content
SpringerLink
Log in

Polytypic Proof Construction

  • Conference paper
  • First Online:
Theorem Proving in Higher Order Logics (TPHOLs 1999)

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

Included in the following conference series:

Abstract

This paper deals with formalizations and verifications in type theory that are abstracted with respect to a class of datatypes; i.e polytypic constructions. The main advantage of these developments are that they can not only be used to define functions in a generic way but also to formally state polytypic theorems and to synthesize polytypic proof objects in a formal way. This opens the door to mechanically proving many useful facts about large classes of datatypes once and for all.

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. B. Barras, S. Boutin, and C. Cornes et. al. The Coq Proof Assistant Reference Manual — Vers. 6.2.4. INRIA, Rocquencourt, 1998.

    Google Scholar 

  2. R. Bird and O. de Moor. Algebra of Programming. International Series in Computer Science. Prentice Hall, 1997.

    Google Scholar 

  3. C. Böhm and A. Berarducci. Automatic Synthesis of Typed λ-Programs on Term Algebras. Theoretical Computer Science, 39:135–154, 1985.

    Article  MathSciNet  MATH  Google Scholar 

  4. T. Coquand and C. Paulin. Inductively Defined Types. In Proc. COLOG 88, volume 417 of LNCS, pages 50–66. Springer-Verlag, 1990.

    Chapter  Google Scholar 

  5. P. Dybjer and A. Setzer. A Finite Axiomatization of Inductive-Recursive Definitions. In J.-Y. Girard, editor, Proc. 4th Int. Conf. on Typed Lambda Calculi and Applications, TLCA’99, volume 1581 of LNCS. Springer-Verlag, 1999.

    Google Scholar 

  6. M. J. C. Gordon and T. F. Melham (eds.). Introduction to HOL: A Theorem Proving Environment for Higher Order Logic. Cambridge University Press, 1993.

    Google Scholar 

  7. R. Harper and R. Pollack. Type Checking, Universal Polymorphism, and Type Ambiguity in the Calculus of Constructions. In TAPSOFT’89, volume II, LNCS, pages 240–256. Springer-Verlag, 1989.

    Google Scholar 

  8. G. Huet and A. Saïbi. Constructive Category Theory. In Proc. CLICS-TYPES Workshop on Categories and Type Theory, January 1995.

    Google Scholar 

  9. C.B. Jay and J.R.B. Cockett. Shapely Types and Shape Polymorphism. In D. Sannella, editor, Programming Languages and Systems — ESOP’94, volume 788 of LNCS, pages 302–316. Springer-Verlag, 1994.

    Google Scholar 

  10. J. Jeuring. Polytypic Pattern Matching. In Conf. Functional Programming Languages and Computer Architecture (FPCA’ 95), pages 238–248. ACM Press, 1995.

    Google Scholar 

  11. J. Jeuring and P. Jansson. Polytypic Programming. In T. Launchbury, E. Meijer, and T. Sheard, editors, Advanced Functional Programming, LNCS, pages 68–114. Springer-Verlag, 1996.

    Chapter  Google Scholar 

  12. Z. Luo. An Extended Calculus of Constructions. Technical Report CST-65-90, University of Edinburgh, July 1990.

    Google Scholar 

  13. Z. Luo and R. Pollack. The Lego Proof Development System: A User’s Manual. Technical Report ECS-LFCS-92-211, University of Edinburgh, 1992.

    Google Scholar 

  14. G. Malcolm. Data Structures and Program Transformation. Science of Computer Programming, 14:255–279, 1990.

    Article  MathSciNet  MATH  Google Scholar 

  15. L. Meertens. Paramorphisms. Formal Aspects of Computing, 4(5):413–425, 1992.

    Article  MATH  Google Scholar 

  16. L. Meertens. Calculate Polytypically. In H. Kuchen and S.D. Swierstra, editors, Programming Languages, Implementations, Logics, and Programs (PLILP’96), LNCS, pages 1–16. Springer-Verlag, 1996.

    Chapter  Google Scholar 

  17. E. Meijer, M. Fokkinga, and R. Paterson. Functional Programming with Bananas, Lenses, Envelopes, and Barbed Wire. In Proc. 5th Conf. on Functional Programming Languages and Computer Architecture, pages 124–144, 1991.

    Google Scholar 

  18. B. Nordström, K. Petersson, and J.M. Smith. Programming in Martin-Löf’s Type Theory. Monographs on Computer Science. Oxford Science Publications, 1990.

    Google Scholar 

  19. Ch.E. Ore. The Extended Calculus of Constructions (ECC) with Inductive Types. Information and Computation, 99,Nr. 2:231–264, 1992.

    Article  MathSciNet  MATH  Google Scholar 

  20. S. Owre, J. Rushby, N. Shankar, and F. von Henke. Formal Verification for Fault-Tolerant Architectures: Prolegomena to the Design of PVS. IEEE Transactions on Software Engineering, 21(2):107–125, 1995.

    Article  Google Scholar 

  21. C. Paulin-Mohring. Inductive Definitions in the System Coq, Rules and Properties. In J.F. Groote M. Bezem, editor, Typed Lambda Calculi and Applications, volume 664 of LNCS, pages 328–345. Springer-Verlag, 1993.

    Chapter  Google Scholar 

  22. L.C. Paulson. A Fixedpoint Approach to (Co)Inductive and (Co)Datatype Definition. Technical report, Computer Laboratory, University of Cambridge, 1996.

    Google Scholar 

  23. H. Rueβ. Computational Reflection in the Calculus of Constructions and Its Application to Theorem Proving. In J. R. Hindley P. de Groote, editor, Proc. 3rd Int. Conf. on Typed Lambda Calculi and Applications TLCA’97, volume 1210 of LNCS, pages 319–335. Springer-Verlag, 1997.

    Chapter  Google Scholar 

  24. N. Shankar. Steps Towards Mechanizing Program Transformations Using PVS. Preprint submitted to Elsevier Science, 1996.

    Google Scholar 

  25. T. Sheard. Type Parametric Programming. Oregon Graduate Institute of Science and Technology, Portland, OR, USA, 1993.

    Google Scholar 

  26. The Lego team. The Lego Library. Distributed with Lego System, 1998.

    Google Scholar 

  27. D. Tuijnman. A Categorical Approach to Functional Programming. PhD thesis, Universität Ulm, 1996.

    Google Scholar 

  28. F. W. von Henke. An Algebraic Approach to Data Types, Program Verification, and Program Synthesis. In Mathematical Foundations of Computer Science, Proceedings, volume 45 of LNCS. Springer-Verlag, 1976.

    Google Scholar 

  29. F. W. von Henke, S. Pfab, H. Pfeifer, and H. Rueβ. Case Studies in Meta-Level Theorem Proving. In Jim Grundy and Malcolm Newey, editors, Proc. Intl. Conf. on Theorem Proving in Higher Order Logics, volume 1479 of LNCS, pages 461–478. Springer-Verlag, September 1998.

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Fakultät für Informatik, Universität Ulm, D-89069, Ulm, Germany

    Holger Pfeifer

  2. Computer Science Laboratory, SRI International, 333 Ravenswood Ave., Menlo Park, CA, 94025, USA

    Harald Rueβ

Authors
  1. Holger Pfeifer
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Harald Rueβ
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. INRIA Sophia Antipolis, 2004 Route des Lucioles, F-06902, Sophia Antipolis Cedex, France

    Yves Bertot , Gilles Dowek  & Laurent Théry ,  & 

  2. University of Nice - Sophia Antipolis, Parc Valrose, F-06108, Nice Cedex 2, France

    André Hirschowitz

  3. University of Paris XI, 15, rue Georges Clemenceau, F-91405, Orsay Cedex, France

    Christine Paulin

Rights and permissions

Reprints and permissions

Copyright information

© 1999 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Pfeifer, H., Rueβ, H. (1999). Polytypic Proof Construction. In: Bertot, Y., Dowek, G., Théry, L., Hirschowitz, A., Paulin, C. (eds) Theorem Proving in Higher Order Logics. TPHOLs 1999. Lecture Notes in Computer Science, vol 1690. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-48256-3_5

Download citation

  • DOI: https://doi.org/10.1007/3-540-48256-3_5

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

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

  • Online ISBN: 978-3-540-48256-7

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation