iris-curry-howard

The Curry-Howard correspondence defines a relationship between programming languages and logical systems. Types correspond to propositions; programs correspond to proofs.

Iris is a logic designed for reasoning about the behavior of concurrent programs. So if we apply the Curry-Howard correspondence to Iris, we should be able to prove the behavior of programs... by writing more programs.

This project is an exploration of that idea.

Versioning

Developed using:

• Coq 8.13.2
• Iris dev.2021-12-17.0.72485828