A logic for Miranda
- 1 March 1989
- journal article
- research article
- Published by Association for Computing Machinery (ACM) in Formal Aspects of Computing
- Vol. 1 (1) , 339-365
- https://doi.org/10.1007/bf01887213
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.Keywords
This publication has 7 references indexed in Scilit:
- Formal methods applied to a floating-point number systemIEEE Transactions on Software Engineering, 1989
- Logic and ComputationPublished by Cambridge University Press (CUP) ,1987
- Laws in MirandaPublished by Association for Computing Machinery (ACM) ,1986
- Categories of partial morphisms and the λP-calculusPublished by Springer Nature ,1986
- Miranda: A non-strict functional language with polymorphic typesLecture Notes in Computer Science, 1985
- Identity and existence in intuitionistic logicPublished by Springer Nature ,1979
- The Design of Well-Structured and Correct ProgramsPublished by Springer Nature ,1978