Abstract
MERILL is a general purpose order-sorted equational reasoning system. Written in Standard ML, it has been developed by the author at the S.E.R.C. Rutherford Appleton Laboratory (RAL) and the Dept of Computing Science at Glasgow University. The development of MERILL was inspired and influenced by the ERIL (Equational Reasoning: an Interactive Laboratory) system developed by Jeremy Dick at RAL and Imperial College, London. This system used order-sorted reasoning in a practical equational reasoning system. However, ERIL was slow, and lacked significant features. MERILL is a entirely new implementation which retains the major features of ERIL whilst being significantly faster and having new facilities. An important extension is the integration of order-sorted reasoning with associated-commutative (AC) operations. The system incorporates more recent work on this, for example. Thus it is comparable with ELIOS-OBJ rather than more traditional rewriting systems. Standard ML was chosen due to its ease of use and of modifiability through its module system, together with the emergence of efficient implementations.
On leave from SERC, Rutherford Appleton Laboratory, Didcot, OXON, OX11 0QX, U.K.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
A J J Dick. ERIL. Equational reasoning: an interactive laboratory. In B. Buchberger, editor, Proceedings of the EUROCAL conference. Springer-Verlag, 1985.
A J J Dick. Order-Sorted Equational Reasoning and Rewrite Systems. PhD thesis, Imperial College, University of London, 1987.
I Gnaedig. ELIOS-OBJ. Theorem proving in a specification language. In B. Kreig-Bruckner, editor, Proc. of ESOP'92, volume 582 of Lecture Notes in Computer Science, pages 182–199. Springer-Verlag, 1992.
I Gnaedig, C Kirchner, and H Kirchner. Equational completion in order-sorted algebras. Theoretical Computer Science, 72:169–202, 1990.
Brian Matthews and Phil Watson. Dynamic order-sorted rewriting. University of Glasgow, in Preparation., 1993.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1993 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Matthews, B. (1993). MERILL: An equational reasoning system in standard ML. In: Kirchner, C. (eds) Rewriting Techniques and Applications. RTA 1993. Lecture Notes in Computer Science, vol 690. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-662-21551-7_34
Download citation
DOI: https://doi.org/10.1007/978-3-662-21551-7_34
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-56868-1
Online ISBN: 978-3-662-21551-7
eBook Packages: Springer Book Archive