Miranda in Isabelle
Stephen Hill and Simon Thompson
Computing Laboratory, University of Kent at Canterbury
Our work has been in using Isabelle to reason about programs written in the
lazy functional programming language Miranda. In our presentation we will
address
- difficulties of translating definitions in the Miranda language
into assertions in Isabelle;
- examples of work done, including larger-scale case studies of
hardware description and refinement (or, from another point of view,
refinement of executable specifications);
- automating the translation of functional programs into logical
assertions;
- reflections on our experience of using Isabelle for this kind of
reasoning.