An interpretation of system F through bar recursion

Valentin Blot

There are two possible computational interpretations of second-order arithmetic: Girard's system F or Spector's bar recursion and its variants. While the logic is the same, the pro…