I've found this webapp which lets you generate a free theorem for a given type.The generated theorems quantify over types and relations on these types. These theorems (formulas) are theorems of which theory/logical system? How does this system relate to the equational theory of the language?
Free theorems, where?
lo.logic;functional programming;type systems;parametricity;logical relations
The formulas are formulas of Abadi-Plotkin logic, which they describe in their paper A Logic for Parametric Polymorphism. The semantics of System F that Abadi and Plotkin used to interpret their logic can be found in Bainbridge, Freyd, Scedrov, Scott's paper Functorial Polymorphism. 