Miranda in Isabelle
Steve Hill, Simon Thompson · Kent Academic Repository (University of Kent) · 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. Miranda1[Turner, 1990, Thompson, 1995b] is a modern functional programming language, al-lowing type polymorphism and higher-order functions in a similar way to ML[Milner et al., 1990]. It differs from ML in being lazy — arguments to functions are only evaluated when and to the extent that they are needed — and in being side-effect free. It has long been an article of faith in the func-tional programming community that languages like this are ideal candidates for program verification because of their ‘declarative ’ nature. This is clearly true for idealised languages, but real languages like Miranda bring their own complexities which we have discussed in the past[Thompson, 1989, Thompson, 1995a]. In this paper we discuss our approaches to formalising proof about Miranda in Isabelle, specifically Isabelle92, after a brief description of the language and how it is given a logical description. 1 Miranda In this section we give a short survey of the main features of Miranda, and how we translate the definitions into logical statements. Full details of a translation can be found in [Thompson, 1989,