A solution of POPLMark challenge with VCPT

Today theorem proving and program properties veri cation are gaining more and more impor- tance. Despite encouraging e orts and progresses achieved in the past years, the use of tools for proving properties and verify theories is still not commonplace. The critical issue is the difficulty to take into account details, rather than conceptual complexity. Furthermore, most proofs are wearisome, long and hard to understand for people lacking of deep knowledge of the problem they are dealing with. On the other hand, new and more powerful tools have been developed in order to build a bridge between the two communities of automated proof developers and programming language designers. It might be the time to reach a good trade o between e orts to formalize language metatheories and results obtained from that process.