Using CafeOBJ to Mechanise Refactoring Proofs and Application. - Antonio Carvalho Júnior; Leila Silva; Márcio Cornélio (SBMF, 2005)