Extend logic with support for multi-shot continuations.

Several changes are performed to the project:

1. The operational semantics of eff_lang now supports both one-shot and multi-shot continuations.

2. The notion of weakest precondition is parameterized by a pair of protocols, one to specify "one-shot effects" and one to specify "multi-shot effects".

3. The project is reorganized into multiple subdirectories: language, where the syntax and semantics of eff_lang is defined; program_logic, where the notion of protocols and the notion of weakest precondition are introduced, and where the reasoning rules of the logic are stated and proved; and case_studies, which contains the adaptation of most of the previous case studies and which contains new case studies such as the implementation and specification of callcc/throw.

4. The theories are consistently and exhaustively documented.