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 ...
Given sets $A$ and $B$, a difunctional relation $(\sim) \subseteq A \times B$ between them is defined to be a relation satisfying the following property: If $a \sim b$ and $a' \sim b'$ and $a \sim ...
I've recently become quite interested in parametricity after seeing Bernardy and Moulin's 2012 LICS paper ( http://www.cse.chalmers.se/~mouling/share/AComputationalInterpretationOfParametricity.pdf). ...
I actually have two questions: Who first used logical relations to relate semantics? I traced them back to Reynold's "On the Relation Between Direct and Continuation Semantics", but I can't claim ...
I'm a beginner working on methods proving program equivalence. I've read a few papers about defining logical relations or simulations to prove two programs are equivalent. But I am quite confused ...