Specify the semantics of mini-protocol programs

input-output-hk / ouroboros-high-assurance

High-assurance implementation of the Ouroboros protocol family

Apache License 2.0

1 stars 1 forks source link

Specify the semantics of mini-protocol programs #94

Closed jeltsch closed 9 months ago

jeltsch commented 11 months ago

We shall specify the semantics of mini-protocol programs as a function from mini-protocol programs to Þ-calculus processes. This approach will allow us to leverage the Þ-calculus for stating and proving properties about mini-protocol behavior.

jeltsch commented 9 months ago

This issue has been superseded by #95 and #96.