A Logic for Miranda, Revisited

Thompson, Simon (1995) A Logic for Miranda, Revisited. Formal Aspects of Computing (7). (Full text available)

PDF
Download (200kB)
[img]
Preview
Postscript
Download (192kB)
[img]
Preview

Abstract

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 > Science Technology and Medical Studies > School of Computing > Theoretical Computing Group
Depositing User: Mark Wheadon
Date Deposited: 21 Aug 2009 19:14
Last Modified: 06 Sep 2011 03:48
Resource URI: http://kar.kent.ac.uk/id/eprint/21271 (The current URI for this page, for reference purposes)
  • Depositors only (login required):

Downloads

Downloads per month over past year