User loginNavigation |
The POPLmark Challenge
(via TYPES)
How close are we to a world where every paper on programming languages is accompanied by an electronic appendix with machine-checked proofs? To gauge progress in this area, we issue here a set of challenge problems, dubbed the POPLmark Challenge, chosen to exercise many aspects of programming languages that are known to be difficult to formalize. A valid solution to the challenge will consist of appropriate software tools, a language representation strategy, and a demonstration that this infrastructure is sufficient to formalize the challenge problems. The POPLmark team explains,
We are not ourselves automated reasoning experts but rather potential users; our impression is that current tools are almost at the point where they can be used routinely. It's time to bring mechanized metatheory to the masses - go to it! |
Browse archives
Active forum topics |
Recent comments
3 weeks 5 days ago
44 weeks 17 hours ago
44 weeks 21 hours ago
44 weeks 21 hours ago
1 year 14 weeks ago
1 year 18 weeks ago
1 year 20 weeks ago
1 year 20 weeks ago
1 year 22 weeks ago
1 year 27 weeks ago