A logic for Miranda
Simon Thompson · Formal Aspects of Computing · 1989
Abstract We formulate a logical description of the functional programming language Miranda. Distinctive features include a full treatment of pattern matching with repeated variables and the characterisation of various (sub-)domains, like the defined natural numbers and finite definite lists, by means of new quantifiers. These quantifiers are introduced by induction rules, and also carry elimination rules. We also discuss the rôle of fixed point induction and issues of modularisation and scale.