AbstractWe discuss how the 1'st order specification and programming language ABEL could be extended with higher order functions. Several issues arise, related to subtyping, parameterization, strictness of generators and defined functions, and to the choice between lambda expressions and currying. The paper can be regarded as an exercise in language design: how to introduce higher order functions under the restrictions enforced by (1'st order) ABEL. A technical result is a soundness proof for covariant subtype replacement, useful when implementing data types under volume constraints imposed by computer hardware.
Categories and Subject Descriptors: D.1.1 [Programming Techniques]: Applicative (Functional) Programming; D.2.1 [Software Engineering]: Requirements/Specifications; D.2.4 [Software Engineering]: Program Verification; D.3.3 [Programming Languages]: Language Constructs and Features; F.3.1 [Logics and Meanings of Programs]: Specifying and Verifying and Reasoning about Programs; F.3.3 [Logics and Meanings of Programs]: Studies of Program Constructs
Additional Key Words and Phrases: algebraic specification, higher order functions, term rewriting, generator induction, parameterized modules, subtypes, strictness.
Selected papers that cite this one
- Ole-Johan Dahl, Olaf Owe, and Tore J. Bastiansen. Subtyping and Constructive Specification. Nordic Journal of Computing, 5(1):19-49, Spring 1998.
Selected references
- Ole-Johan Dahl, Olaf Owe, and Tore J. Bastiansen. Subtyping and Constructive Specification. Nordic Journal of Computing, 5(1):19-49, Spring 1998.
- Dale Miller. A logic programming language with lambda-abstraction, function variables, and simple unification. Journal of Logic and Computation, 1(4):497-536, September 1991.