Adjust paper to ESOP format.

Adjusting paper to the ESOP format

We change the format of our previous POPL submission to the ESOP format.

Here is the list of the most important changes:

1. Introduction Section.
   The introduction is completely rewritten, now stressing that we address the aliasing challenge.

2. Set of examples.
   We keep the examples of the function counter (and its variants), filter, and lex-handle; we add the new example of the function mix; and we remove the example of the function reassemble, which was defined as reassemble f = handle f() with yield: fun x k -> x :: k() | fun _ -> [] (and which could perhaps be named collect instead).

3. Purity attributes.
   We remove purity attributes from the paper presentation of Tes. We present the standard value restriction instead. As a consequence, we do not need to have a stratified notion of wp indexed by a purity attribute. The wp definition in the case indexed by the marker P did not use update modalities (nor did it use the logical state), thus endowing this notion of a strong reasoning principle, the infinitary conjunction rule, which allows one to hoist a universal quantification from the postcondition to the root of wp.

4. Name of the logic and of the calculus.
   Following a suggestion from one of our POPL reviewers, we rename lambda-labels into TesLang and Hazel+ into TesLogic.

Side note

We also rename some the subrepository theories/hazel to theories/logic, which is a more neutral option than the previous one.