Wolfram Kahl, Claudia Hattensperger
pp. 140--164 in Bettina Buth, Rudolf Berghammer, Jan Peleska (eds.):
Program Systems for Computer-Aided System Development and Verification,
Vol. 1 of BISS Monographs, Shaker Verlag Aachen, 1998,
ISBN: 3-8265-3806-4
(.bib, .ps.gz)
HOPS and RALF are two interactive symbol manipulation systems -- one for functional programming and program transformation, the other for proving relation algebraic formulae -- that both implement interactive application of second-order rewriting rules, \HOPS on term graphs and RALF on conventional terms and formulae. Both systems support a larger class of second-order rewriting rules than commonly found in other systems.
In this paper we provide a homogeneous underpinning to second-order syntax and rewriting for easing the transition from terms to term graphs and vice versa, so that aspects that are easier to understand in one view also further understanding in the other view, altogether making a case for bringing second-order syntax more directly to the user interface than usual in most systems today.
Also refer to the HOPS and RALF home pages.