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 182-196, September 1995.


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

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 = {},
    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: 21/03/2014