# 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*](https://iris-project.org/) 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