Skip to main content

A Logic for Miranda, Revisited

Thompson, Simon (1995) A Logic for Miranda, Revisited. Formal Aspects of Computing, (7). (KAR id:21271)

Language: English
Download (365kB) Preview
Language: English
Download (192kB) Preview


This paper expands upon work begun in the author's paper 'A Logic for Miranda', Formal Aspects of Computing 1 (1989), 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 the earlier paper 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. This paper has been accepted for publication in Formal Aspects of Computing.

Item Type: Article
Subjects: Q Science > QA Mathematics (inc Computing science) > QA 76 Software, computer programming,
Divisions: Faculties > Sciences > School of Computing > Theoretical Computing Group
Depositing User: Mark Wheadon
Date Deposited: 21 Aug 2009 19:14 UTC
Last Modified: 23 Jan 2020 04:04 UTC
Resource URI: (The current URI for this page, for reference purposes)
Thompson, Simon:
  • Depositors only (login required):


Downloads per month over past year