Abstract
We present a constructive theory of types and kinds (called TK5) designed with program development as the major desideratum. We motivate its definition with respect to existing research in the area of program logics (in particular Martin-Lof's theory of types) and establish suitable infrastructure for program extraction from proofs of specifications.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
5 References
Abbas, A., Programming with types and rules in Martin Lof's theory of types PhD thesis, London Univeristy, 1987
Beeson, M., Formalising constructive mathematics: why and how? Constructive mathematics: proceedings, New Mexico, 1980, Lecture Notes in Mathematics, Vol 873, pp 146–90, Springer, 1981
Beeson, M., Foundations of constructive mathematics Springer-Verlag, 1985
Beeson, M., Proving programs and programming proofs Logic, Methodology and Philosophy of Science VII, Elsevier, pp 51–82, 1986
Beeson M., Towards a computation system based on set theory, Tech. Report. Dept. Maths and Computer Science, San Jose State University
Burstall, R. and Lampson, B., A kernel language for abstract data types and modules Symp. on semantics of data types, Lecture notes in computer science, Vol. 173, pp 1–50, Springer, 1984
Constable, R., et.al., Implementing Mathematics with the NuPRL proof development system, Prentice Hall, 1986
Feferman, S., A language and axioms for explicit mathematics Algebra and Logic, Lecture notes in mathematics, Vol. 450, pp 87–139, North Holland, Amsterdam, 1975
Hayashi, S., The PX system — a computational logic University of Tokyo, tech rep. 1987
Henson, M. C., Elements of functional languages, Blackwells, 1987
Henson, M. C., Program development in the constructive set theory TK5 submitted for publication and University of Essex, tech rep. No. 110, 1988
Hindley, J. R. and Seldin, J. P., Introduction to combinators and lambda calculus London Math. Soc. students texts, Vol. 1, Cambridge, 1986
Khamiss, A. Algorithm development in Martin-Lof's theory of types PhD thesis, University of Essex, 1986
Kleene, S., On the interpretation of intuitionistic number theory J. Symb. logic., Vol. 10, pp 109–24, 1945
Kreisel, G. and Troelstra, A., Formal systems for some branches of intuitionistic analysis Annals of Math. logic, Vol. 1, pp 229–387, 1979
Leivant, D., Polymorphic type inference Proc. 10th ACM symp. on principles of programming languages, 1983
McQueen D. and Sethi, R., A semantic model of types for applicative languages Proc. ACM conf. on LISP and functional programming, pp 243–52, 1982
Malcolm, G. and Chisholm, P., Polymorphism in Martin-Lof's type theory, Private Communication, Unpublished notes, Rijksuniversiteit Groningen, 1988
Martin-Lof, P., An intuitionistic theory of types: predicative part Logic Coll. 73, North-Holland, Amsterdam, 1975
Martin-Lof, P., Preprint of [Martin-Lof 82], Report No. 11 University of Stockholm, 1979
Martin-Lof, P., Constructive Mathematics and Computer Programming Logic, Methodology and Philosophy of Science VI, pp 153–179, North Holland, Amsterdam, 1982
Mitchell, J. and Plotkin, G., Abstract types have existential type Proc. 12th ACM conf. on principles of programming languages, pp 37–51, 1985
Mohring, C., Algorithm development in the calculus of constructions Proc. IEEE symp. on logic in computer science, 1986
Nordstrom, B., Terminating general recursion Tech rep., University of Goteborg, Programming Methodology Group, 1987
Peyton-Jones, S., The implementation of functional programming languages Prentice Hall, 1987
Reynolds, J. C., Towards a theory of type structures Proc. Programming symposium, Lecture notes in computer science, Vol. 19, Springer, 1974
Turner, D., A new implementation technique for applicative languages Software, Practice and Experience, Vol. 9, pp 31–49, 1979
Turner, D., Miranda: a non strict functional language with polymorphic types Proc. Conf. on functional programming and computer architecture, Lecture notes in computer science, Vol. 201, Springer, 1985
Turner, R., A theory of properties J. Symb. logic, Vol. 52, No. 2, pp 445–472, 1987
Turner, R., Combinatory logic and type theory via stable truth submitted for publication and University of Essex, tech rep. 109, 1988
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1988 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Henson, M.C., Turner, R. (1988). A constructive set theory for program development. In: Nori, K.V., Kumar, S. (eds) Foundations of Software Technology and Theoretical Computer Science. FSTTCS 1988. Lecture Notes in Computer Science, vol 338. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-50517-2_89
Download citation
DOI: https://doi.org/10.1007/3-540-50517-2_89
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-50517-4
Online ISBN: 978-3-540-46030-5
eBook Packages: Springer Book Archive