The paper presents a specification of sequent calculi and natural deduction proofs and a description of the transformation between them. The language expressing the above is a subset of higher-order hereditary Harrop formulas which correspond to \(\lambda\)Prolog. The specification itself presents both a declarative and an operational description of the correspondence between the sequent calculus and natural deduction for intuitionistic logic, which can actually be run as a program in \(\lambda\)Prolog.
For the entire collection see [Zbl 0770.68025].