The goal of automated refactoring is to reduce maintenance effort. To realize this, programmers need to be able to trust or manually check that refactorings actually preserve behavior. To allow programmers to focus on such checks, automated refactorings should preserve program well-typedness. However, historically automated refactorings in popular IDEs could break well-typedness. The reason is that modern languages have complex name binding semantics which makes it hard to guarantee well-typedness in general.

So how do we prove well-typedness preservation of a refactoring?