School of Computing

A Logic for Miranda, Revisited

Simon Thompson

Formal Aspects of Computing, (7):182-196, March 1995.

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.

Download publication 79 kbytes

Bibtex Record

@article{63,
author = {Simon Thompson},
title = {{A Logic for Miranda, Revisited}},
month = {March},
year = {1995},
pages = {182-196},
keywords = {determinacy analysis, Craig interpolants},
note = {},
doi = {},
url = {http://www.cs.kent.ac.uk/pubs/1995/63},
    journal = {Formal Aspects of Computing},
    number = {7},
}

School of Computing, University of Kent, Canterbury, Kent, CT2 7NF

Enquiries: +44 (0)1227 824180 or contact us.

Last Updated: 21/03/2014