On the implementation of abstract data types by programming language constructs
type: Item
instance of: scholarly article
title: On the implementation of abstract data types by programming language constructs
zbMATH Open document ID: 0619.68025
DOI: 10.1016/0022-0000(87)90029-8
author: Axel Poigné
author: Josef Voss
published in: Journal of Computer and System Sciences
publication date: 1987-01-01T00:00:00Z
review text: Implementations of abstract data types are defined via enrichments of a target type. We propose to use an extended typed \(\lambda\)-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 \(\lambda\)-calculus which seem to be of interest in their own right.
Mathematics Subject Classification ID: 68P05
zbMATH DE Number: 4005597
zbMATH Keywords: typed \(\lambda \)-calculus
zbMATH Keywords: correctness
MaRDI profile type: Publication
full work available at URL: 0022-0000(87)90029-8
OpenAlex ID: W2166482687
cites work: Initial Algebra Semantics and Continuous Algebras
cites work: Q3342534
cites work: Q3741042
cites work: Implementation of data types by algebraic methods
cites work: Q3871894
cites work: Generalized algebraic theories and contextual categories
cites work: Q3785893
cites work: Algebraic implementation of abstract data types
cites work: Parameter passing in algebraic specification languages
cites work: The Expressiveness of Simple and Second-Order Type Structures
cites work: Q3727946
cites work: Q4743722
cites work: Abstract data types and algebraic semantics of programming languages
cites work: Q3707388
cites work: On specifications, theories, and models with higher types
cites work: Q3677152
cites work: Combinators, \(\lambda\)-terms and proof theory
cites work: Intensional interpretations of functionals of finite type I
cites work: Q3666260
description: scientific article; zbMATH DE number 4005597