IntersectMBO / plutus

The Plutus language implementation and tools
Apache License 2.0
1.57k stars 479 forks source link

ForceDelay Extra Proofs #6529

Open ramsay-t opened 1 month ago

ramsay-t commented 1 month ago

Phil Wadler suggests some proofs to show the correspondence of the decidable definition of FD to the more clearly semantically valid pureFD.