© University of Kent - Contact | Feedback | Legal | FOI | Cookies
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 182-196, 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 kbytesBibtex Record
@inproceedings{209,
author = {Steve Hill and Simon Thompson},
title = {Miranda in {I}sabelle},
month = {September},
year = {1995},
pages = {182-196},
keywords = {determinacy analysis, Craig interpolants},
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},
}