[This post is by Frank Fu.] I have recently written up a note with a reducibility proof for call-by-value (CBV) System F.
You can get one from my website: http://www.cs.uiowa.edu/~pfu/
This may be useful for those interested in how one shows termination of System F by the reducibility method.
My note is based on Girard’s proof, showing strong normalization for System F with full beta-reduction. Here are the differences between this version of proof and Girard’s proof:
0. Restrict on CBV closed terms.
1. Eleminate the types at the term level, so the interpretation of the universal abstract type reflects a notion of ’intersection type’.
2. Reducible terms are not assumed to be typable.
3. Add a constant to the term to construct inactive terms, which makes the reducibility set to be non-empty.
4. Comments from Prof. Stump: The interpretation of every type is required to be non-empty is not flexible enough for some of the type theories we are interested in, since certain types really are expected to have empty interpretations (for example, equality types
like 0 = 1). Still, I think it was an excellent exercise to explore
this approach, and to discover what it can handle and what it cannot.