Programs and types
- 1 October 1980
- proceedings article
- Published by Institute of Electrical and Electronics Engineers (IEEE)
- p. 118-128
- https://doi.org/10.1109/sfcs.1980.36
Abstract
The first two sections of this paper motivate and outline a constructive theory of (data) types which we developed for formal program verification. The executable component of the theory provides a very high level programming language with a rich type structure. A theory of this generality appears necessary to manage complex programming and formal reasoning about it. The logical component, influencea by AUTOMATH and LCF and based on Martin-Löf's ITT, appears strong enough to formalize constructive mathematics; hence a theory or this generality is probably sufficient for program development and verification. The last two sections of the paper illustrate the richness of the theory and the benefits of generality by describing with it different "denotational" semantics for programs. Because the theory is constructive, these abstract semantics are also computational.Keywords
This publication has 30 references indexed in Scilit:
- First-Order Dynamic LogicLecture Notes in Computer Science, 1979
- Abstract data types and software validationCommunications of the ACM, 1978
- Is “sometime” sometimes better than “always”?Communications of the ACM, 1978
- Complexity of finitely presented algebrasPublished by Association for Computing Machinery (ACM) ,1977
- Recursive data structuresInternational Journal of Parallel Programming, 1975
- Specification techniques for data abstractionsIEEE Transactions on Software Engineering, 1975
- Automatic program verification I: A logical basis and its implementationActa Informatica, 1975
- An introduction to the set theoretical language SETLComputers & Mathematics with Applications, 1975
- PASCAL User Manual and ReportPublished by Springer Nature ,1975
- Recursively defined data typesPublished by Association for Computing Machinery (ACM) ,1973