Abstract
We discuss some of the boons as well as shortcomings of constructive type theory as a foundation for computer science. Certain new concepts are offered for tailoring these theories to this task including an idea for collecting objects into subtypes and a proposal for using logic variables and treating them as part of the definition of the logic.
This research supported by NSF grant CCR86-16552 and ONR grant N00014-88K-0490.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
S. F. Allen. A non-type-theoretic semantics for type-theoretic language. PhD thesis, Cornell University, 1987.
S. F. Allen. A non-type-theoretic definition of martin-löf's types. Proc. of Second Symp. on Logics in Computer Science, IEEE, pages 215–224., June 1987.
P. Audebaud. Partial objects in the calculus of constructions. In Sixth Symp. on Logic in Computer Science, IEEE, Vrije University, Amsterdam, The Netherlands, 1991.
D. Basin and R. Constable. Meta-logical frameworks. In Proc. of the Second Workshop on Logical Frameworks, Edinburgh, UK, June 1991.
J. L. Bates. A logic for correct program development. PhD thesis, Cornell University, 1979.
E. Bishop and D. Bridges. Constructive Analysis. NY:Springer-Verlag, 1985.
W. Buchholtz et al. Iterated inductive definitions and subsystems of analysis. Recent Proof-Theoretical Studies, Lecture Notes in Mathematics, 897, 1981.
R. Constable and N. Mendler. Recursive Definitions in Type Theory. In Proc. of Logics of Prog. Conf., pages 61–78, January 1985. Cornell TR 85-659.
R. Constable and S. F. Smith. Computational foundations of basic function theory. In Third Symp. on Logic in Somp. Sci. IEEE, 1988. (Cornell TR 88–904).
R. L. Constable et al. Implementing Mathematics with the Nuprl Development System. NJ:Prentice-Hall, 1986.
T. Coquand and G. Huet. The calculus of construction. Information and Computation, 76:95–120., 1988.
S. Feferman. Formal theories for transfinite iterations of generalized inductive definitions and some subsystems of analysis. In Proc. Conf. Intuitionism and Proof Theory, pages 303–326, Buffalo, NY, 1970. North-Holland.
J.-Y. Girard. Une extension de l'interpretation de godel a l'analyse, et son application a l'elimination des coupures dans l'analyse et la theorie des types. In 2nd Scandinavian Logic Symp., pages 63–69. NY:Springer-Verlag, 1971.
J.-Y. Girard, Y. Lafont, and P. Taylor. Proofs and Types. Cambridge University Press, 1988.
M. Gordon, R. Milner, and C. Wadsworth. Edinburgh LCF: a mechanized logic of computation. Lecture Notes in Computer Science, 78, 1979.
T. Griffin. A formulas-as-types notion of control. In POPL, 1990.
S. Hayashi and H. Nakano. PX: A Computational Logic. Foundations of Computing. MIT Press, Cambridge, MA, 1988.
D. J. Howe. Automating Reasoning in an Implementation of Constructive Type Theory. PhD thesis, Cornell University, 1988.
D. J. Howe. Equality in lazy computation systems. Proc. Fourth Symp. Logic in Computer Science, IEEE, 1989.
J. Lipton. Logic programming in the nuprl type theory environment. Technical report, Cornell University, Ithaca, NY, 1991. To appear as a technical report, summer 1991.
Z. Luo. Ecc, an extended calculus of construction. In Proc. Fourth Symp. on Logics in Computer Science, IEEE, Washington, DC, June 1989.
P. Martin-Lof. An intuitionistic theory of types: predicative part. In Logic Colloquium '73., pages 73–118. Amsterdam:North-Holland, 1973.
P. Martin-Lof. Constructive mathematics and computer programming. In Sixth International Congress for Logic, Methodology, and Philosophy of Science, pages 153–75. Amsterdam:North Holland, 1982.
P. Mendler. Recursive Types and Type Constraints in Second-Order Lambda Calculus. Proc. in Second Symp. on Logic in Comp. Sci., IEEE, pages 30–36, June 1987.
P. Mendler. Inductive Definition in Type Theory. PhD thesis, Cornell University, Ithaca, NY, 1988.
C. Murthy. Extracting Constructive Content for Classical Proofs. PhD thesis, Cornell University, Dept. of Computer Science, 1990. TR 89-1151.
C. Murthy. An evaluation semantics for classical proofs. In LICS, '91, Amsterdam, The Netherlands, July 1991.
C. Murthy and J. Russell. A constructive proof of higman's lemma. Technical Report TR 89-1049, Cornell University, Ithaca, NY 14853, January 1989.
B. Nordstrom, K. Peterson, and J. Smith. Programming in Martin-Lof's Type Theory. Oxford Sciences Publication, Oxford, 1990.
C. Paulin-Mohring. Extraction in the calculus of constructions. PhD thesis, University of Paris VII, 1989.
R. Pollack. Lego user's guide. Technical report, University of Edinburgh, 1990.
S. Smith. Partial Objects in Type Theory. PhD thesis, Cornell University, Ithaca, NY, 1989.
S. F. Smith and R. L. Constable. Partial objects in constructive type theory. In Symposium on Logic in Computer Science., pages 183–93. Washington, D.C.:IEEE., 1987.
R. M. Smullyan. First-Order Logic. Springer-Verlag, New York, 1968.
J. Underwood. A constructive completeness proof for the intuitionistic propositional calculus. Technical report, Cornell University, 1990.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1991 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Constable, R.L. (1991). Type theory as a foundation for computer science. In: Ito, T., Meyer, A.R. (eds) Theoretical Aspects of Computer Software. TACS 1991. Lecture Notes in Computer Science, vol 526. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-54415-1_48
Download citation
DOI: https://doi.org/10.1007/3-540-54415-1_48
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-54415-9
Online ISBN: 978-3-540-47617-7
eBook Packages: Springer Book Archive