On the implementation of abstract data types by programming language constructs

摘要

Implementations of abstract data types are defined via enrichments of a target type. We propose to use an extended typed λ-calculus for enrichments in order to meet the conceptual requirement that an implementation has to bring us closer to a (functional) program. Composability of implementations is investigated, the main result being that composition of correct implementations is correct if terminating programs are implemented by terminating programs. Moreover, we provide syntactical criteria to guarantee correctness of composition. The proof is based on strong normalization and Church-Rosser results of the extended λ-calculus which seem to be of interest in their own right.