7. Österreichische Artificial-Intelligence-Tagung / Seventh Austrian Conference on Artificial Intelligence pp 126-136 | Cite as

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

Conference paper

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

## References

- [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 - [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 - [BCM89]R.C. Backhouse, P. Chisholm, and G. Malcolm. Do-it-yourself Type Theory.
*Formal Aspects of Computing*, 1:19–84, 1989.CrossRefGoogle Scholar - [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 - [Con86]R.L. Constable et al. Implementing Mathematics with the Nuprl Proof Development System. Prentice-Hall, 1986.Google Scholar
- [GMW79]M.J.C. Gordon, R. Milner, and C.P. Wadsworth.
*Edinburgh LCF*. Springer-Verlag LNCS, 78, 1979.zbMATHCrossRefGoogle Scholar - [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 - [Hen89]M. C. Henson. Program development in the constructive set theory TK.
*Formal Aspects of Computing*, 1:173–192, 1989.MathSciNetCrossRefGoogle Scholar - [HN87]S. Hayashi and H. Nakano.
*PX, a Computational Logic*. Technical Report, Research Institute for Mathematical Science, Kyoto University, 1987.Google Scholar - [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 - [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 - [Mil78]R. Milner. A Theory of Type Polymorphism in Programming Languages.
*Journal of Computer and System Sciences*, 17:348–375, 1978.MathSciNetzbMATHCrossRefGoogle Scholar - [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 - [NPS90]B. Nordstrom, K. Petersson, and J. Smith.
*Programming in Martin-Löf’s Type Theory*. Clarendon Press, Oxford, 1990.Google Scholar - [Pet82]K. Petersson.
*A programming system for type theory*. LPM Memo 21, Department of Computer Science, Chalmers University of Technology, Goteborg, 1982.Google Scholar - [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 - [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