A logic for Miranda, revisited
Simon Thompson · Formal Aspects of Computing · 1995
Abstract This paper expands upon work begun in [Tho89], in building a logic for the Miranda functional programming language. After summarising the work in that paper, a translation of Miranda definitions into logical formulas is presented, and illustrated by means of examples. This work expands upon [Tho89] in giving a complete treatment of sequences of equations, and by examining how to translate the local definitions 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 definitions into conditional equations. Finally it is shown how the logic can be implemented in the Isabelle proof tool.