DOI: 10.1093/logcom/exag051 ISSN: 0955-792X
Church- and Curry-typing in the meaning explanations of constructive type theory
Bruno Bentzen, Ansten KlevAbstract
The distinction between Church- and Curry-style typing is well established in type theory. In the Church style, the type of a term is intrinsic to it and determines with which other terms it may be combined in the construction of complex terms. In the Curry style, the type of a term is extrinsic to it and does not influence the rules of term formation. Martin-Löf’s meaning explanations for constructive type theory turn out to be sensitive to this distinction. We spell out a Church and a Curry interpretation of the meaning explanations and shed light on some philosophical differences between them.