[plt-scheme] writing a proof checker

Background: I have HtDP-level knowledge of PLT Scheme, but I haven't
explored all the nice packages and extensions yet. I'm looking for
pointers on how to proceed with a small problem.

I'm teaching a course in logic and computation, and we have just
finished covering natural deduction for propositional logic. Here is
an example of the kind of thing we are asking students to do,
translated into pure text.

Sequent:

p /\ q -> r |- p -> (q -> r)

Proof:

1  p /\ q -> r    premise
    [
2    p            assumption
      [
3       q         assumption
4       p /\ q    /\i 2,3
5       r         ->e 1,4
      ]
6    q->r         ->i 3-5
    ]
7  p->(q->r)      ->i 2-6

As you can see, lines are numbered, and each contains a formula and a
justification. The justification is either "premise" (occurs on the
LHS of the sequent), "assumption" (at the top of a proof box, opened
with [ and closed with ], which is my way of representing boxes drawn
around all the lines thus bracketed), or the application of a proof
rule to earlier lines or sequences of lines. For example, line 5
applies ->e to p/\q->r and p/\q to yield r. Line 6 applies ->i,
concluding q->r from the proof box starting with the assumption q on
line 3 and ending with r on line 5. Formulas are partly
deparenthesized for readability by using precedence among logical
connectives: ~ (not), then /\ and \/ (and, or), then ->. I'm not wed
to the exact textual representation, but it should be reasonably close
to the typeset symbols (that is, I don't want to represent formulas by
S-expressions).

If I wanted to write a PLT Scheme program which read a proof such as
the one above and checked it for validity, with informative error
messages, what would be the simplest way to proceed? I know how to go
at it frontally using Beginning Student, but there's no need for me to
reinvent the wheel.

I don't think I want to actually ask students to do this in lieu of
submitting handwritten proofs, but it's a good way for me to learn
more about what PLT Scheme offers. Thanks. --PR

(PS Natural deduction for predicate logic is coming up soon.)