A logic for Miranda, revisited

Abstract This paper expands upon work begun in the authors Tho in building a logic for the Miranda functional programming language After sum marising the work in that paper a translation of Miranda denitions into logical formulas is presented and illustrated by means of examples This work expands upon Tho in giving a complete treatment of sequences of equations and by examining how to translate the local denitions introduced by where clauses The status of the logic is then examined and it is argued that the logic extends a natural operational semantics of Miranda given by the translations of denitions into conditional equations Finally it is shown how the logic can be implemented in the Isabelle proof too