Skip to main content
SpringerLink
Log in

Recursive definitions in type theory

  • Conference paper
  • First Online:
Logics of Programs (Logic of Programs 1985)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 193))

Included in the following conference series:

Abstract

We offer a new account of recursive definitions for both types and partial functions. The computational requirements of the theory restrict recursive type definitions involving the total function-space constructor (→) to those with only positive occurrences of the defined typed. But we show that arbitrary recursive definitions with respect to the partial function-space constructor are sensible. The partial function-space constructor allows us to express reflexive types of Scott's domain theory (as needed to model the lambda calculus) and thereby reconcile parts of domain theory with constructive type theory.

This work was supported in part by NSF grant MCS81-04018

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Allen, Stuart. The logical foundations of type theory. (To appear as Cornell Ph.D. thesis.)

    Google Scholar 

  2. Aczel, P. An introduction to inductive definitions. Handbook of Mathematical Logic, Barwise, J. (ed.), North Holland, NY (1977) 739–782.

    Google Scholar 

  3. Bates, J.L. and Constable, R.L. Proofs as programs. TOPLAS, January 1985.

    Google Scholar 

  4. Bishop, E., Foundations of Constructive Analysis. McGraw Hill, New York, NY, 1967. 370 pp.

    Google Scholar 

  5. Boyer, R.S. and Moore, J.S. A Computational Logic. Academic Press, New York, NY, 1979. 397 pp.

    Google Scholar 

  6. Brouwer, L.E.J. Collected Works, Vol. 1, A. Heyting, (Ed.), North-Holland, 1975.

    Google Scholar 

  7. Cartwright, R. User-defined data types as an aid to verifying Lisp programs. Proc. of the 3rd Int'l. Colloq. on Automata, Languages and Programming, [Michaelson, S. and Milner, R., eds.], Edinburgh University Press, Edinburgh (1976) 228–256.

    Google Scholar 

  8. Cartwright, R. Toward a logical theory of program data. In Logics of Programs, Lecture Notes in Computer Science 131, Springer-Verlag, New York, NY (1982) 37–51.

    Google Scholar 

  9. Church, A. A formulation of the simple theory of types. J. Symbolic Logic, 5, (1940), 56–68.

    Google Scholar 

  10. Constable, Robert L. Constructive mathematics and automatic program writers. In Proc. of IFIP Congress, Ljubljana, 1971, 229–233.

    Google Scholar 

  11. Constable, Robert L. Constructive mathematics as a programming logic I: some principles of theory. Technical report TR83-554, Dept. of Computer Science, Cornell University, May 1983. (To appear in Proc. of FCT Conf., Springer-Verlag, 1983).

    Google Scholar 

  12. Constable, Robert L. Partial functions in constructive formal theories. In Proc. of 6th G.I. Conference, Lecture Notes in Computer Science 45, Springer-Verlag, New York, NY, 1983.

    Google Scholar 

  13. Constable, R.L., and Bates, J.L. The nearly ultimate PRL. Tech. Rep., Dept. of Computer Science, Cornell University, TR 83-551, 1984.

    Google Scholar 

  14. Constable, Robert L. and O'Donnell, M.J. A Programming Logic. Winthrop, Cambridge, 1978.

    Google Scholar 

  15. Constable, Robert L. and Zlatin, D.R. The type theory of PL/CV3. ACM Trans. on Prog. Lang. & Syst., 6:1 (Jan. 1984) 94–117.

    Google Scholar 

  16. Constable, Robert L. Mathematics as programming. In Proc. of Workshop on Logics of Programs,Lecture Notes in Computer Science 164, Springer-Verlag, New York, NY, 1983, 116–128.

    Google Scholar 

  17. Curry, H.B., Hindley, J.R. and Seldin, J.P. Combinatory Logic, Volume II. North-Holland Publ. Co., Amsterdam, 1972.

    Google Scholar 

  18. deBruijn, N.G. A survey of the project AUTOMATH. In To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, J.P. Seldin and J.R. Hindley (Eds.), Academic Press, New York, NY, 1980, 579–607.

    Google Scholar 

  19. Demers, A.J. and Donahue, J. Revised report on Russell. Tech. Rep., Department of Computer Science, Cornell University, TR 79-389, September 1979.

    Google Scholar 

  20. Feferman, S. Formal theories for transfinite iterations of generalized inductive definitions and some subsystems of analysis, Intuitionism and Proof Theory, Kino, A., Myhill, J., and Vesley, R.E. (eds.), North Holland, Amsterdam (1970) 303–326.

    Google Scholar 

  21. Girard, J.-Y. Interpretation Fonctionelle et Elimination des Coupures de l'arithmeétique d'ordre supérieur. Ph.D. Thesis, Univ. of Paris VII, 1972.

    Google Scholar 

  22. Gordon, M., Milner, R., and Wadsworth, C. Edinburgh LCF: A Mechanized Logic of Computation, Lecture Notes in Computer Science 78, Springer-Verlag, 1979.

    Google Scholar 

  23. Harper, R. Aspects of the implementations of type theory. Ph.D. thesis, Computer Science Department, Cornell University, NY, June 1985.

    Google Scholar 

  24. Hoare, C.A.R. Recursive data structures. International Journal of Computer and Information Sciences, 4:2, (June 1975), 105–132.

    Google Scholar 

  25. Kleene, S.C. Introduction to Metamathematics. D. Van Nostrand, Princeton, NJ, 1952.

    Google Scholar 

  26. Kleene, S.C. Formalized recursive functionals and formalized realizability. Memoirs of the American Math. Society, No. 89, 1969.

    Google Scholar 

  27. Kreisel, G. Generalized inductive definitions, section III. Standard report on the foundations of analysis (mimeographed), 1963.

    Google Scholar 

  28. Knuth, D.E. The Art of Computer Programming, Vol. I. Addison-Wesley, Reading, 1968.

    Google Scholar 

  29. MacQueen, D.B., Plotkin, Gordon D. and Sethi, R. An Ideal Model for Recursive Polymorphic Types. 11th ACM Symp. on Principles of Programming Languages, (1984) 165–174.

    Google Scholar 

  30. MacQueen, D.B., and Sethi, R. A semantic model of types for applicative languages. ACM Symp. on LISP and Functional Programming, 1982, 243–252.

    Google Scholar 

  31. Martin-Löf, Per. Constructive mathematics and computer programming. In 6th International Congress for Logic, Methodology and Philosophy of Science, North-Holland, Amsterdam, 1982.

    Google Scholar 

  32. Martin-Löf, P. Hauptsatz for the intuitionistic theory of iterated inductive definitions. In Proceedings of the Second Scandinavian Logic Symposium, J.E. Fenstad (Ed.), North-Holland, Amsterdam, 1971, 179–216.

    Google Scholar 

  33. McCarty, David C. Realizability and recursive mathematics. Computer Science Dept. Tech. Rpt. CMU-CS-84-131, Carnegie-Mellon University (1984).

    Google Scholar 

  34. McGettrick, A.D. Algol 68, A First and Second Course. Cambridge University Press, Cambridge, 1978.

    Google Scholar 

  35. Meyer, Albert R. What is a model of the lambda calculus? Information and Control, 52, (1982), 87–122.

    Google Scholar 

  36. Moschovakis, Yiannis N. Elementary Induction on Abstract Structures. North Holland, London, 1974.

    Google Scholar 

  37. Plotkin, Gordon D. Tw as a universal domain. J. Computer and System Sciences, 17, (1978), 209–236.

    Google Scholar 

  38. Plotkin, Gordon D. Private communication.

    Google Scholar 

  39. PRL Staff, The. Constructing proofs: An introduction to the Nuprl proof development system. Computer Science Department, Cornell University, January 1985.

    Google Scholar 

  40. Quine, Willard Van Orman. Set Theory and Its Logic. Harvard University Press, Cambridge, 1963.

    Google Scholar 

  41. Reynolds, John C. Types, abstraction, and parametric polymorphism. Information Processing 83, IFIP, North Holland Publishers, 1983, 513–523.

    Google Scholar 

  42. Russell, B. Mathematical logic as based on a theory of types. Am. J. of Math., 30, (1908), 222–262.

    Google Scholar 

  43. Scott, Dana. Data types as lattices. SIAM Journal on Computing, 5:3 (September 1976) 522–587.

    Google Scholar 

  44. Scott, Dana. The lambda calculus, some models, some philosophy. The Kleene Symposium [eds., J. Barwise, et al.], North-Holland, 1980, 381–421.

    Google Scholar 

  45. Scott, Dana. Constructive validity. In Symposium on Automatic Demonstration, Lecture Notes in Mathematics 125, Springer-Verlag, 1970, 237–275.

    Google Scholar 

  46. Stenlund, S. Combinators, Lambda-terms, and Proof-Theory. D. Reidel, Dordrecht, 1972, 183.

    Google Scholar 

  47. Stoy, Joseph E. Denotational Semantics: The Scott-Strachey Approach to Programming Language Theory. MIT Press, Cambridge, MA, 1977.

    Google Scholar 

  48. Tait, William W. Intensional interpretation of functionals of finite type. J Symbolic Logic, 32:2, (June 1967), 198–212.

    Google Scholar 

  49. van Heijenoort, Jean. From Frege to Gödel: A source book in mathematical logic, 1879–1931, Harvard University Press, Cambridge (1967).

    Google Scholar 

  50. van Wijngaarden, A.B.J. et al. Revised report on the algorithmic language ALGO 68. Acta Informatica, 5, (1975), 1–236. (Also a Supplement to ALGO BULLETIN, University of Alberta, 1974.)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Computer Science Department, Cornell University, 14853, Ithaca, N. Y.

    R. L. Constable & N. P. Mendler

Authors
  1. R. L. Constable
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. N. P. Mendler
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Rohit Parikh

Rights and permissions

Reprints and permissions

Copyright information

© 1985 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Constable, R.L., Mendler, N.P. (1985). Recursive definitions in type theory. In: Parikh, R. (eds) Logics of Programs. Logic of Programs 1985. Lecture Notes in Computer Science, vol 193. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-15648-8_5

Download citation

  • DOI: https://doi.org/10.1007/3-540-15648-8_5

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-15648-2

  • Online ISBN: 978-3-540-39527-0

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation