Interactive Proof Checking
Thomas Reps and Bowen Alpern
Knowledge of logical inference rules allows a specialized proof editor
to provide a user with feedback about errors in a proof under
development. Providing such feedback involves checking a collection
of constraints on the strings of the proof language. Because
attribute grammars allow such constraints to be expressed in a
modular, declarative fashion, they are a suitable underlying formalism
for a proof-checking editor. This paper discusses how an attribute
grammar can be used in an editor for partial-correctness program
proofs in Hoare-style logic, where verification conditions are proved
using the sequent calculus.
Cornell University