Programming with theorem-proving and online judges?

Google Group
1

Dear All,

has anyone here considered how programming with theorem-proving could be
incorporated into an automated online judge like UVa, SPOJ, COJ…?

It would seem to me that when dataprops are provided by the problem setter,
that would not be so hard. But how about when developing the specifications
is part of the problem to be solved? Would it even be doable?

Best,

Marko

2

has anyone here considered how programming with theorem-proving could be
incorporated into an automated online judge like UVa, SPOJ, COJ…?

I have not. I designed some problems for my students for which well-typed
solutions are guaranteed to be correct.

In the past, I used PwTP to solve some problems published at the following
site:

I think this is a great way to learn PwTP.

I was told about this by Guillaume Brunerie. Unfortunately, his page is no
longer accessible:

http://www.eleves.ens.fr/home/brunerie/ats_euler.en.html

If you are interested, it would be a good idea to create a webpage (using
github?) and then
publish some dataprops for selected problems. My hunch is that quite a few
people interested
in ATS would like to contribute solutions as well as problems.On Wednesday, December 3, 2014 12:31:09 PM UTC-5, Marko Schütz-Schmuck wrote:

Dear All,

has anyone here considered how programming with theorem-proving could be
incorporated into an automated online judge like UVa, SPOJ, COJ…?

It would seem to me that when dataprops are provided by the problem
setter, that would not be so hard. But how about when developing the
specifications is part of the problem to be solved? Would it even be doable?

Best,

Marko

3

I was told about this by Guillaume Brunerie. Unfortunately, his page is no
longer accessible:

http://www.eleves.ens.fr/home/brunerie/ats_euler.en.html

Seems there is a backup at the Internet Archive, but I can’t tell for sure,
as I can’t display anything as it looks very slow.

4

Forget the link :
https://web.archive.org/web/20111116031643/http://www.eleves.ens.fr/home/brunerie/ats_euler.en.htmlLe mercredi 3 décembre 2014 20:53:07 UTC+1, Yannick Duchêne a écrit :

Le mercredi 3 décembre 2014 20:01:22 UTC+1, gmhwxi a écrit :

I was told about this by Guillaume Brunerie. Unfortunately, his page is
no longer accessible:

http://www.eleves.ens.fr/home/brunerie/ats_euler.en.html

Seems there is a backup at the Internet Archive, but I can’t tell for
sure, as I can’t display anything as it looks very slow.

5

A repository of programming challenges together with sandboxed machinery
that will compile and test submissions to those challenges. There are
usually several possible verdicts: accept, wrong answer, presentation
error, time-limit exceeded, memory limit exceeded, and possibly more.

Take a look at uva.onlinejudge.org or coj.uci.cu.On Wednesday, December 3, 2014 3:54:28 PM UTC-4, Yannick Duchêne wrote:

What is an “online judge”?

Le mercredi 3 décembre 2014 18:31:09 UTC+1, Marko Schütz-Schmuck a écrit :

Dear All,

has anyone here considered how programming with theorem-proving could be
incorporated into an automated online judge like UVa, SPOJ, COJ…?

It would seem to me that when dataprops are provided by the problem
setter, that would not be so hard. But how about when developing the
specifications is part of the problem to be solved? Would it even be doable?

Best,

Marko

6

What is an “online judge”?Le mercredi 3 décembre 2014 18:31:09 UTC+1, Marko Schütz-Schmuck a écrit :

Dear All,

has anyone here considered how programming with theorem-proving could be
incorporated into an automated online judge like UVa, SPOJ, COJ…?

It would seem to me that when dataprops are provided by the problem
setter, that would not be so hard. But how about when developing the
specifications is part of the problem to be solved? Would it even be doable?

Best,

Marko