Fully abstract compilation from System F to lambda-seal

We describe our work-in-progress on applying the technique of approximate back-translation in order to prove a theorem that was conjectured in a number of papers. The theorem is that a compiler from System~F to lambda-seal which uses sealing primitives for enforcing parametricity achieves full abstraction. We describe our work in progress, challenges we faced and ideas about solutions.status: publishe