Bruno Bentzen: Untyped and typed evaluation in the meaning explanations

Organized by the Department of Logic

Further information

Bruno Bentzen (Zhejiang University): Untyped and typed evaluation in the meaning explanations

Abstract:

There are two main styles of typing in type theory. Under Church-style, every expression has a built-in type that is one of its intrinsic properties, just as a fingerprint is a built-in trait of a person's identity. Under Curry-style, types are assigned to preexisting expressions of an untyped universe, just like a passport can be used to identify a person after their birth. My aim in this talk is to shed light on this distinction in the context of two remarkably different versions of the meaning explanations developed by Martin-Löf for his constructive type theory. More precisely, I want to contrast his early 1979 lower-order formulation of the meaning explanations based on untyped evaluation with his late higher-order formulation assuming typed evaluation exposed in his 1993 Leiden lectures. I argue that the adoption of typed evaluation in the late formulation gives rise to a circular explanation of what it is for something to be an element of a set or a proof of a proposition.