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.


Developed using:

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