 While accepting Sundholm’s point, we keep the terms themselves, considering that they have perhaps become too common to change.  Section 5.3  below is the appropriate place to explain our preference for “Proof Interpretation” over “BHK-Interpretation”.