platform icon indicating copy to clipboard operation
platform copied to clipboard

Coq platform for research artifact evaluation

Open palmskog opened this issue 5 years ago • 22 comments

The research communities around programming languages, formal methods, and software engineering are continually expanding and improving artifact evaluation for their premier conferences. Some examples:

The Coq platform is a natural focal point for research artifacts based on Coq and OCaml. Researchers can potentially target a Coq platform version for their submitted artifact, and this platform version is then used by the committee during artifact evaluation, which minimizes packaging and distribution effort for both parties, and ensures reproducibility. The Coq platform can also provide a format for packaging the artifacts for long-time archiving.

However, Coq platform maintainers will likely have to coordinate with artifact evaluation committee chairs so that the Coq platform is permitted as part of mandated evaluation environments. For example, a virtual machine may be mandated which does not directly support the Coq platform without significant work by the submitting researchers.

Since the POPL AE traditionally has many Coq artifacts, e.g., around 10 out of 40 artifacts submitted during 2019, coordinating with the chairs of that committee is a natural first step.

palmskog avatar Jan 19 '20 03:01 palmskog

As do CPP and ITP of course.

spitters avatar Mar 17 '20 17:03 spitters

To my knowledge, neither CPP nor ITP have a dedicated artifact evaluation committee, and doesn't currently provide any guidelines that restrict how artifacts are submitted or handled by any committees. This is why I believe we would have much better success in getting Coq platform adoption to the POPL artifact evaluation.

palmskog avatar Mar 17 '20 18:03 palmskog

This would be great; just to add more data, in POPL 2020, 17 out of the 40 artifacts used Coq.

tchajed avatar Jul 15 '20 22:07 tchajed

@palmskog : I am not sure what to do about this. Would you consider this solved by the recent paper by you, @gares and @Zimmi48 ?

MSoegtropIMC avatar Mar 21 '22 19:03 MSoegtropIMC

@MSoegtropIMC our paper is only one piece of the puzzle in convincing venues such as TACAS, CPP, etc., to recommend submissions to use the Platform whenever they have a Coq artifact. I expect that the academic side of the Platform team will have to "evangelize" using the Platform for several years more. Hence, I think we should keep this issue open to track progress.

palmskog avatar Mar 21 '22 19:03 palmskog

OK, I created a milestone "Longterm"

MSoegtropIMC avatar Mar 21 '22 20:03 MSoegtropIMC