On Exploiting the Structure of Martin-Löf’s Theory of Types
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.
Unable to display preview. Download preview PDF.
- [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
- [Con86]R.L. Constable et al. Implementing Mathematics with the Nuprl Proof Development System. Prentice-Hall, 1986.Google 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
- [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
- [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