LMCS.md

## Examples

The examples of the original POPL20 paper are covered in
[papers/POPL20.md](POPL20.md).

The following list gives a mapping between the additional examples in the
paper and their mechanization in Coq:

Introduction
  - Swapping program: [theories/examples/basics.v](../theories/examples/basics.v)
Subprotocols
  - Basics: [theories/examples/subprotocols.v](../theories/examples/subprotocols.v)
  - Mapper: [theories/examples/swap_mapper.v](../theories/examples/swap_mapper.v)
  - List reversal: [theories/examples/list_rev.v](../theories/examples/list_rev.v)
  - Löb recursion: [theories/examples/subprotocols.v](../theories/examples/subprotocols.v)
Mechanisation
  - Program: [theories/examples/basics.v](../theories/examples/basics.v)
  - Subprotocol: [theories/examples/list_rev.v](../theories/examples/list_rev.v)