A solution of POPLMark Challenge with VCPT
Today theorem proving and program properties verification are gaining more and more importance.
Despite encouraging efforts 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 off between efforts to formalize language metatheories and results obtained from that process.