Mentions légales du service

Skip to content

Bring formalisation closer to the paper

DE VILHENA Paulo Emílio requested to merge popl21-paper into master

A number of changes is proposed with the purpose of bringing the formalisation closer to the presentation found in the paper. These modifications are mainly four:

  1. The fancy update modalities are removed from the definition of protocol_agreement.

  2. The protocol subsumption iEff_le is redefined in terms of the more abstract notion of protocol_agreement.

  3. The later modalities in the definitions of both shallow_handler and deep_handler are replaced to give rise to correctness judgements that are easier to prove.

  4. The verification of the scheduler is revised.

Merge request reports