Related to this question

I'm wondering, what is the standard technique for showing that dependent types with eliminators are strongly normalizing? I'm thinking something like the Calculus of Inductive Constructions, or Dybjer-style inductive families. I've heard that they are strongly normalizing. For example, in dependent pattern matching, compiling to eliminators is touted as a way of getting guaranteed termination.

I've seen the standard logical relations approach for non-dependent-type systems (Godel's system T) as well as System F, and I've seen hereditary substitution for dependent types without inductives (i.e. LF). But I've never seen the two combined.

What's the standard technique for proving that these calculi are strongly normalizing? Do logical relations work, and if so, what do you have to do to get the inductive-measure to work? (i.e. step-indexing, structural-indexing, multiset-orderings, etc.)



Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.