School of Computing

Miranda in Isabelle

Steve Hill and Simon Thompson

In Lawrence C. Paulson, editor, Preceedings of the first Isabelle Users Workshop, number 397 in University Of Cambridge Computer Laboratory Technical Reports Series, pages 122-135, September 1995.

Abstract

This paper describes our experience in formalising arguments about the Miranda functional programming language in Isabelle. After explaining some of the problems of reasoning about Miranda, we explain our two different approaches to encoding Miranda in Isabelle. We conclude by discussing some shorter examples and a case study of reasoning about hardware.

Download publication 31 kbytes

Bibtex Record

@inproceedings{209,
author = {Steve Hill and Simon Thompson},
title = {Miranda in {I}sabelle},
month = {September},
year = {1995},
pages = {122-135},
keywords = {Miranda verification Isabelle},
note = {},
doi = {},
url = {http://www.cs.kent.ac.uk/pubs/1995/209},
    booktitle = {Preceedings of the first Isabelle Users Workshop},
    editor = {Lawrence C. Paulson},
    number = {397},
    refereed = {no},
    series = {University Of Cambridge Computer Laboratory Technical Reports Series},
}

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

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

Last Updated: 12/03/2012 17:02