What technique is used to implement type checking for CoC?

Question

I am studying David Christiansen's tutorial on implementing a dependently typed language, where it says:

Typed normalization by evaluation is far from the only way to implement conversion checking for dependent types. Indeed, normalization by evaluation has a number of characteristics that make it only suitable for certain theories: it η-expands expressions as many times as possible, but η-expansion is not valid for some theories (including Coq’s Calculus of Constructions)

1. May I have a reference to why η expansion is invalid for CoC? Is there some "moral" by which one can see the rules of CoC and realise that η expansion is invalid?
2. The rules for implementing CoC in ATAPL Chapter 2 look to my naive eye like NBE (Normalization by Evaluation). The rules for CoC are given as an extension to the equivalence rules of LF, augmented with extra rules that govern how Prf (the encoding mechanism of Pi types) and Prop interact. The rules QA-NABS-1, QA-NABS-2 seem to be implementing η expansion for stuck terms? Why do these rules not describe NBE?
3. Is there a name for the rules given in ATAPL to implement type checking for CoC? They seem ad-hoc to me, and I don't understand how I would come up with them. I would appreciate a reference to the framework that is used to create the reduction rules for CoC (for clarity, by a framework, I refer to ideas such as NBE or hereditary substitution)

I have included the rules for CoC as given in ATAPL, Chapter 2, for reference:

Answer 1

May I have a reference to why η expansion is invalid for CoC?

It's not invalid. It's up to choice whether $\eta$-conversion for functions (or other types) is included. The original CoC paper seems to omit it, but as you see ATAPL includes it. I'm not certain, but $\eta$ may have been omitted from the original source because it was difficult to handle in the strong normalization arguments, back in the days. Nowadays normalization proofs are more likely to be based on NbE themselves, and have no issues with $\eta$-rules. Modern Coq definitely has $\eta$ for functions, and it is generally considered a highly useful basic feature.

The rules QA-NABS-1, QA-NABS-2 seem to be implementing η expansion for stuck terms? Why do these rules not describe NBE?

They do specify $\eta$ for functions. It's not really NbE though. ATAPL only describes how to compare weak head normal forms for conversion in an iterated fashion, it does not say how to efficiently compute to whnf. The essential part of NbE is the separation of syntax and values; this is missing from the ATAPL exposition.

Indeed, normalization by evaluation has a number of characteristics that make it only suitable for certain theories: it η-expands expressions as many times as possible

This is incorrect. NbE is not necessarily type-directed, and does not necessarily include $\eta$-expansion. If you look at QA-NABS-1, QA-NABS-2 and the other rules in ATAPL, they can be adapted to a conversion checking algorithm on NbE values, which is a) purely syntax-directed b) does not require $\eta$-expansion in evaluation c) decides $\eta$-conversion for functions.

Is there a name for the rules given in ATAPL to implement type checking for CoC? They seem ad-hoc to me, and I don't understand how I would come up with them.

I'm not aware of any rigorous and generic way for specifying conversion checking algorithms. I would summarize the rules of thumbs as follows.

The specification of values is obtained from the specification of syntax by replacing binders with metalanguage functions or closures. Evaluation goes from syntax to values and performs $\beta$-reduction (but not necessarily $\eta$-conversions). Then, conversion checking can be implemented on values, proceeding purely structurally, except where we want syntax-directed $\eta$-checking in the manner specified in ATAPL.

Answer 2

I have a shorter answer: normalization is usually used in conversion check of terms (aka definitional equality), and CoC has untyped conversion check. In conversion check, we normalize terms and compare 'em syntactically (think of it as comparing the ASTs). This probably means the normalization process doesn't have access to the types of terms, so it may not be able to expand the terms into eta-long normal forms.

OTOH, the intuitionistic type theory by Martin Lof has typed conversion check. IMO this is also the reason why homotopy type theory chose intuitionistic type theory as the type theory framework it uses.