Spike: Type-checked specification

input-output-hk / hydra

Implementation of the Hydra Head protocol

https://hydra.family/head-protocol/

Apache License 2.0

264 stars 86 forks source link

Open ch1bo opened 2 weeks ago

ch1bo commented 2 weeks ago

@locallycompact TODO complete

Identify whether a more consistent type-checked specification is feasible with Agda.

Related to #1187 and #843

Literate Agda with LaTeX source
A few of the preliminary types / definitions from https://hydra.family/head-protocol/docs/dev/specification/
- e.g. Transaction outputs
CI action which type-checks and produces a PDF

ch1bo commented 2 weeks ago

@locallycompact Can you please link the repository you created here?

locallycompact commented 2 weeks ago