Proposal to move Polaris to coq-community

[palmskog]

Project name: Polaris

Initial author(s): Joseph Tassarotti

Current URL: https://github.com/jtassarotti/polaris

Kind: pure Coq library

License: BSD

Description: Library for reasoning about probabilistic and concurrent programs, based an extension of the Iris project for probabilistic and relational reasoning.

Status: Appears to be unmaintained (doesn't work with Coq 8.9 or 8.10).

New maintainer: looking for a volunteer

@jtassarotti can you can you comment on the status of Polaris and whether (or not) you believe this project could be a good fit for Coq-community? To my knowledge, the only other modern formalization of probability is in the infotheo project.

[jtassarotti]

Thanks for your interest in this project, Karl. I have broken out the library for probability theory into a separate repo (https://github.com/jtassarotti/coq-proba) under Apache 2.0, and I am maintaining that (and extending it even, contributions welcome). It should build against 8.9.1.

I imagine most of the general interest is in this part of the library, so in light of that perhaps there is not much steam for moving the rest of polaris into coq-community. (But, I indeed ought to update polaris to point to this external repo.)

[palmskog]

@jtassarotti thanks for flagging up the proba project. We would very much encourage submitting OPAM (2.0) packages for it here for better dissemination in the community.

It still looks to me like it could be a good student project to refactor/generalize the non-proba Polaris code for maintainability - preserving the paper artifact. So if you don't mind, I'll keep the issue open here.