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 archivesActive forum topics |
Recent comments
5 days 6 hours ago
4 weeks 6 days ago
5 weeks 3 days ago
5 weeks 3 days ago
7 weeks 3 days ago
7 weeks 3 days ago
7 weeks 6 days ago
7 weeks 6 days ago
8 weeks 6 days ago
9 weeks 5 days ago