Equivalence in functional languages with effects
- 1 July 1991
- journal article
- Published by Cambridge University Press (CUP) in Journal of Functional Programming
- Vol. 1 (3) , 287-327
- https://doi.org/10.1017/s0956796800000125
Abstract
Traditionally the view has been that direct expression of control and store mechanisms and clear mathematical semantics are incompatible requirements. This paper shows that adding objects with memory to the call-by-value lambda calculus results in a language with a rich equational theory, satisfying many of the usual laws. Combined with other recent work, this provides evidence that expressive, mathematically clean programming languages are indeed possible.Keywords
This publication has 14 references indexed in Scilit:
- Reasoning about programs with effectsPublished by Springer Nature ,2005
- Syntactic control of interference Part 2Published by Springer Nature ,1989
- Programming, transforming, and proving with function abstractions and memoriesPublished by Springer Nature ,1989
- Verification of programs that destructively manipulate dataScience of Computer Programming, 1988
- Polymorphic effect systemsPublished by Association for Computing Machinery (ACM) ,1988
- Side effects and aliasing can have simple axiomatic descriptionsACM Transactions on Programming Languages and Systems, 1985
- Reasoning about recursively defined data structuresPublished by Association for Computing Machinery (ACM) ,1978
- Viewing control structures as patterns of passing messagesArtificial Intelligence, 1977
- Call-by-name, call-by-value and the λ-calculusTheoretical Computer Science, 1975
- The Mechanical Evaluation of ExpressionsThe Computer Journal, 1964