A bisimulation for type abstraction and recursion
We present a bisimulation method for proving the contextual equivalence of packages in λ-
calculus with full existential and recursive types. Unlike traditional logical relations (either
semantic or syntactic), our development is “elementary,” using only sets and relations and
avoiding advanced machinery such as domain theory, admissibility, and TT-closure. Unlike
other bisimulations, ours is complete even for existential types. The key idea is to consider
sets of relations—instead of just relations—as bisimulations.
calculus with full existential and recursive types. Unlike traditional logical relations (either
semantic or syntactic), our development is “elementary,” using only sets and relations and
avoiding advanced machinery such as domain theory, admissibility, and TT-closure. Unlike
other bisimulations, ours is complete even for existential types. The key idea is to consider
sets of relations—instead of just relations—as bisimulations.
We present a bisimulation method for proving the contextual equivalence of packages in λ-calculus with full existential and recursive types. Unlike traditional logical relations (either semantic or syntactic), our development is “elementary,” using only sets and relations and avoiding advanced machinery such as domain theory, admissibility, and TT-closure. Unlike other bisimulations, ours is complete even for existential types. The key idea is to consider sets of relations—instead of just relations—as bisimulations.
ACM Digital Library