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.