Publisher： Cambridge University Press
E-ISSN： 1943-5886|49|3|730-753
ISSN： 0022-4812
Source： The Journal of Symbolic Logic, Vol.49, Iss.3, 1984-09, pp. : 730-753
Disclaimer: Any content in publications that violate the sovereignty, the constitution or regulations of the PRC is not accepted or approved by CNPIEC.
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.
Related content
Access to resources
Recommend
A construction of non-well-founded sets within Martin-Löf's type theory
The Journal of Symbolic Logic, Vol. 54, Iss. 1, 1989-03 ,pp. :
A type-free Gödel interpretation
The Journal of Symbolic Logic, Vol. 43, Iss. 2, 1978-06 ,pp. :
The generalised type-theoretic interpretation of constructive set theory
The Journal of Symbolic Logic, Vol. 71, Iss. 1, 2006-06 ,pp. :