Advertisement

On Exploiting the Structure of Martin-Löf’s Theory of Types

  • Andrew Ireland
Conference paper
Part of the Informatik-Fachberichte book series (INFORMATIK, volume 287)

Abstract

Program synthesis in Martin-Löf’s Theory of Types is a theorem proving activity. We demonstrate how the rich structure of the theory may be exploited in the automation of this activity. Basic properties of data type constructors are shown to exhibit a general structure in the way in which they are expressed and derived. A proof procedure for negation is developed based upon these properties. As a consequence our proof procedure may be extended uniformly to incorporate new data types.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. [Bac86]
    R.C. Backhouse. On the Meaning and Construction of the Rules in Martin- Löf’s Theory of Types. Computing Science Notes CS 8606, Dept. of Mathematics and Computing Science, University of Groningen, 1986.Google Scholar
  2. [Bac87]
    R.C. Backhouse. Overcoming the mismatch between programs and proofs. In P. Dybjer, B. Nordstrom, K. Petersson, and J.M. Smith, editors, Proceedings of the Workshop in Programming Logic, pages 116–122, Marstrand, June 1987.Google Scholar
  3. [BCM89]
    R.C. Backhouse, P. Chisholm, and G. Malcolm. Do-it-yourself Type Theory. Formal Aspects of Computing, 1:19–84, 1989.CrossRefGoogle Scholar
  4. [Chi87]
    P. Chisholm. Derivation of a Parsing Algorithm in Martin-Löf’s Theory of Types. Science of Computer Programming, 8:1–42, 1987.MathSciNetzbMATHCrossRefGoogle Scholar
  5. [Con86]
    R.L. Constable et al. Implementing Mathematics with the Nuprl Proof Development System. Prentice-Hall, 1986.Google Scholar
  6. [GMW79]
    M.J.C. Gordon, R. Milner, and C.P. Wadsworth. Edinburgh LCF. Springer-Verlag LNCS, 78, 1979.zbMATHCrossRefGoogle Scholar
  7. [Ham85]
    A.G. Hamilton. Program Construction in Martin-Löf Type Theory. Technical Report, T.R. 24, Dept. of Computing Science, University of Stirling, June 1985.Google Scholar
  8. [Hen89]
    M. C. Henson. Program development in the constructive set theory TK. Formal Aspects of Computing, 1:173–192, 1989.MathSciNetCrossRefGoogle Scholar
  9. [HN87]
    S. Hayashi and H. Nakano. PX, a Computational Logic. Technical Report, Research Institute for Mathematical Science, Kyoto University, 1987.Google Scholar
  10. [Ire89]
    A. Ireland. Mechanization of Program Construction in Martin-Löf’s Theory of Types. PhD thesis, Dept. of Computing Science, University of Stirling, 1989.Google Scholar
  11. [Mar82]
    P. Martin-Löf. Constructive Mathematics and Computer Programming. In L.J. Cohen, J. Los, H. Pfeiffer, and K-P. Podewski, editors, Logic, Methodology and Philosophy of Science F2, pages 153–175, North-Holland, 1982.CrossRefGoogle Scholar
  12. [Mil78]
    R. Milner. A Theory of Type Polymorphism in Programming Languages. Journal of Computer and System Sciences, 17:348–375, 1978.MathSciNetzbMATHCrossRefGoogle Scholar
  13. [Moh89]
    C. Mohring. Extracting Fas programs from proofs in the Calculus of Constructions. In Proceedings of the 16 th ACM Symposium of Principles of Programming Languages, pages 89–104, 1989.Google Scholar
  14. [NPS90]
    B. Nordstrom, K. Petersson, and J. Smith. Programming in Martin-Löf’s Type Theory. Clarendon Press, Oxford, 1990.Google Scholar
  15. [Pet82]
    K. Petersson. A programming system for type theory. LPM Memo 21, Department of Computer Science, Chalmers University of Technology, Goteborg, 1982.Google Scholar
  16. [PM89]
    F. Pfenning and C. Mohring. Inductively defined types in the Calculus of Constructions. Presented at: Mathematical foundations of programming language semantics, 1989.Google Scholar
  17. [Smi87]
    J. Smith. On a Nonconstructive Type Theory and Program Derivation. In D.G. Skordev, editor, Mathematical Logic and its Applications, pages 331–340, Plenum Publishing Corporation, 1987.CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1991

Authors and Affiliations

  • Andrew Ireland
    • 1
  1. 1.Department of Artificial IntelligenceUniversity of EdinburghEdinburghScotland

Personalised recommendations