Thompson, Simon (1995) A Logic for Miranda, Revisited. Formal Aspects of Computing, (7). (KAR id:21271)
PDF
Language: English |
|
Download this file (PDF/200kB) |
![]() |
Request a format suitable for use with assistive technology e.g. a screenreader | |
Postscript
Language: English |
|
Download this file (Postscript/192kB) |
Preview |
Request a format suitable for use with assistive technology e.g. a screenreader |
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: | Divisions > Division of Computing, Engineering and Mathematical Sciences > School of Computing |
Depositing User: | Mark Wheadon |
Date Deposited: | 21 Aug 2009 19:14 UTC |
Last Modified: | 16 Nov 2021 09:59 UTC |
Resource URI: | https://kar.kent.ac.uk/id/eprint/21271 (The current URI for this page, for reference purposes) |
- Link to SensusAccess
- Export to:
- RefWorks
- EPrints3 XML
- BibTeX
- CSV
- Depositors only (login required):