Extend logic with support for multi-shot continuations.
Several changes are performed to the project:
-
The operational semantics of
eff_lang
now supports both one-shot and multi-shot continuations. -
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".
-
The project is reorganized into multiple subdirectories:
language
, where the syntax and semantics ofeff_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; andcase_studies
, which contains the adaptation of most of the previous case studies and which contains new case studies such as the implementation and specification ofcallcc/throw
. -
The theories are consistently and exhaustively documented.