The tag has no wiki summary.

learn more… | top users | synonyms

8
votes
2answers
595 views

Free theorems, where?

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 ...
8
votes
1answer
183 views

Uses of quasi-PERs/difunctional relations/zig-zag relations?

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 ...
9
votes
4answers
396 views

Unary parametricity vs. binary parametricity

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). ...
15
votes
2answers
518 views

What is the origin of logical relations?

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 ...
21
votes
4answers
2k views

What are the differences between logical relations and simulations?

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 ...