The identification of propositions and types in Martin-Löf's type theory: A programming example

  • Jan Smith
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 158)


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    E.Bishop, Foundations of Constructive Analysis (McGraw-Hill 1967).Google Scholar
  2. 2.
    E.Bishop, Mathematics as a numerical language, Myhill, Kino and Vesley, eds., Intuitionism and Proof Theory pp.53–71 (North-Holland 1970).Google Scholar
  3. 3.
    R.M.Burstall, D.B.McQueen and D.T.Sanella, Hope: An experimental applicative language, Proceedings of the 1980 LISP conference, pp.136–143.Google Scholar
  4. 4.
    R.Constable, Constructive Mathematics and Automatic Program Writers, Information Processing 71 (North-Holland 1972).Google Scholar
  5. 5.
    M.J.Gordon, A.J.Milner and C.P.Wadsworth, Edinburgh LCF, Lecture Notes in Computer Science 78 (Springer-Verlag 1979).Google Scholar
  6. 6.
    K. Gödel, Über eine bisher noch nicht benütze Erweiterung des finiten Standpunktes, Dialectica, Vol. 12, 1958, pp.280–287.Google Scholar
  7. 7.
    A.Heyting, Intuitionism, an introduction (North-Holland 1956).Google Scholar
  8. 8.
    S.C.Kleene, Introduction to Metamathematics (North-Holland 1952).Google Scholar
  9. 9.
    Z. Manna and R. Waldinger, A deductive approach to program synthesis, ACM Transactions on Programming Languages and Systems, Vol.2, No.1, pp.92–121, 1980.Google Scholar
  10. 10.
    P.Martin-Löf, An Intuitionistic Theory of Types: Predicative Part, Logic Colloquium 73, Rose and Shepardson, eds., pp.73–118 (North-Holland 1975).Google Scholar
  11. 11.
    P.Martin-Löf, Constructive Mathematics and Computer Programming, Logic, Methodology and Philosophy of Science VI, pp.153–175 (North-Holland 1982).Google Scholar
  12. 12.
    B.Nordström, Programming in Constructive Set Theory, Some Examples, Proceedings of the Conference on Functional Programming Languages and Computer Architecture, ACM, Portsmouth, New Hampshire 1981.Google Scholar
  13. 13.
    K. Petersson, A programming system for type theory, LPM Memo 21, 1982, Dept. of Computer Science, Chalmers Univ. of Technology, Göteborg, Sweden.Google Scholar
  14. 14.
    D.Turner, SASL Language Manual, St.Andrews University, Technical report 1976.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1983

Authors and Affiliations

  • Jan Smith
    • 1
  1. 1.Department of Computer ScienceUniversity of Göteborg Chalmers University of TechnologyGöteborgSweden

Personalised recommendations