Abstract
In this paper we discuss some practical aspects of using type theory as a programming and specification language, where the viewpoint is to use it not only as a basis for program synthesis but also as a programming language with a programming logic allowing us to do ordinary verification.
The subset type has been added to type theory in order to avoid irrelevant information in programs. We give an example of a proof which illustrates the problems that may occur if the subset type is used in specifications when we have the standard interpretation of propositions as types. Harrop-formulas and Squash are then discussed as solutions to these problems. It is argued that they are not acceptable from a practical point of view.
An extension of the theory to include the two new judgment forms:A is a proposition, andA is true, is then given and explained in terms of the old theory. The logical constants are no longer identified with the corresponding type theoretical constants, but propositions are interpreted as Gödel formulas, which allow us to introduce and justify logical rules similar to rules for classical logic. The interpretation is extended to include predicates defined by using reflections of the ordinary definition of Gödel formulas in a “type of small propositions”.
The programming example is then revisited and stronger elimination rules are discussed.
This is a preview of subscription content, log in via an institution to check access.
Similar content being viewed by others
References
R. Backhouse,Overcoming the mismatch between programs and proofs. Proceedings of the Workshop on Programming Logic, Marstrand, Sweden, 1987.
M. J. Beeson,Foundation of Constructive Mathematics, Springer-Verlag Berlin-Heidelberg 1985.
R. Dykhof,Strong elimination rules in type theory. Proceedings of the Workshop on Programming Logic, Marstrand, Sweden, 1987.
S. Hayashi and H. Nakano,PX: A computational Logic, Foundation of Computing Series, MIT Press 1989.
R. Harrop,Concerning formulas of the types A → B ∨ C, A → (Ex)B(x) in intuitionistic formal series. Journal of Symbolic Logic Vol. 25, No. 1, March 1960, pp. 27–32.
G. Malcolm and P. Chisholm,Polymorphism and Information Loss in Martin-Löf's Type Theory. Computing Science Notes, University of Groningen, The Netherlands.
P. Martin-Löf,Intuitionistic Type Theory. Studies in Proof Theory, Lecture Notes, Bibliopolis, Napoli, 1984.
C. Mohring,Extracting F w 's programs from proofs in the calculus of constructions, ACM 1989.
B. Nordström and K. Petersson,Types and specifications. In Proceedings IFIP'83, Paris, pp. 915–920. Elsevier, Amsterdam 1983.
B. Nordström, K. Petersson and J. M. Smith,Programming in Martin-Löf's Type Theory. An Introduction. Monograph. In preparation. To be published by Oxford University Press.
The Prl Staff (R. Constable et al.),Implementing Mathematics with The Nuprl Proof Development System. Prentice-Hall, 1986.
A. Salvesen,Stable propositions in Martin-Löf's extensional type theory. In Ph.D. Thesis, University of Oslo, Norway 1989.
A. Salvesen and J. M. Smith,The Strength of the Subset Type in Martin-Löf's Type Theory. Proceedings of the Third Annual Symposium on Logic in Computer Science, Edinburgh, Scotland, 1988, (IEEE).
J. M. Smith,On a Nonconstructive Type Theory and Program Derivation. To appear in the proceedings of Conference on Logic and its Applications, Bulgaria 1986 (Plenum Press).
A. S. Troelstra,Notions of Realizability. In Proceedings of the Second Scandinavian Logic Symposium, pp. 369–405. North-Holland, Amsterdam, 1971.
A. S. Troelstra,Metamathematical Investigation of Intuitionistic Arithmetic and Analysis. Lecture Notes in Mathematics, No. 344, Springer-Verlag, 1973.