Hostname: page-component-8448b6f56d-sxzjt Total loading time: 0 Render date: 2024-04-19T11:52:36.196Z Has data issue: false hasContentIssue false
  • English
  • Français

An interpretation of Martin-Löf's type theory in a type-free theory of propositions

Published online by Cambridge University Press:  12 March 2014

Jan Smith
Jan Smith*
Affiliation:
Chalmers University of Technology and University of Göteborg, 412 96 Göteborg, Sweden
Get access Rights & Permissions [Opens in a new window]

Abstract

We present a formal theory of propositions and combinator terms, and in this theory we give an interpretation of Martin-Löf's type theory. The construction of the interpretation is inspired by the semantics for type theory, but it can also be viewed as a formalized realizability interpretation.

Type
Research Article
Information
The Journal of Symbolic Logic , Volume 49 , Issue 3 , September 1984 , pp. 730 - 753
Copyright
Copyright © Association for Symbolic Logic 1984

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

References

REFERENCES

[1]Aczel, P.. The strength of Martin-Löf's intuitionistic type theory with one universe, Proceedings of the symposium on mathematical logic (Oulu, 1974), Report No. 2, Department of Philosophy, University of Helsinki, Helsinki, 1977, pp. 1–32.Google Scholar
[2]Aczel, P., Frege structures and the notions of proposition, truth and set, The Kleene Symposium, North-Holland, Amsterdam, 1980, pp. 31–59.CrossRefGoogle Scholar
[3]Beeson, M., Recursive models for constructive set theories, Annals of Mathematical Logic, vol. 23 (1983), pp. 127–178.CrossRefGoogle Scholar
[4]Martin-Löf, P.. An intuitionistic theory of types, Logic Colloquium '73, North-Holland, Amsterdam, 1975, pp. 73–118.Google Scholar
[5]Martin-Löf, P., Constructive mathematics and computer programming, Logic, Methodology and Philosophy of Science VI, North-Holland, Amsterdam, 1982, pp. 153–175.Google Scholar
[6]Smith, J.. On the relation between a type theoretic and a logical formulation of the theory of constructions, Dissertation, Department of Mathematics, University of Göteborg, Göteborg, 1978.Google Scholar