Abstract types have existential type

Abstract data type declarations appear in typed programming languages like Ada, Alphard, CLU and ML. This form of declaration binds a list of identifiers to a type with associated operations, a composite "value" we call a data algebra. We use a second-order typed lambda calculus SOL to sho...

Full description

Saved in:
Bibliographic Details
Published in:ACM transactions on programming languages and systems 1988-07, Vol.10 (3), p.470-502
Main Authors: Mitchell, John C., Plotkin, Gordon D.
Format: Article
Language:English
Subjects:
Applied sciences
Computer science
control theory
systems
Exact sciences and technology
Formal language definitions
Program semantics
Programming languages
Semantics
Semantics and reasoning
Software
Software and its engineering
Software notations and tools
Theory of computation
Citations: Items that this one cites
Items that cite this one
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary:Abstract data type declarations appear in typed programming languages like Ada, Alphard, CLU and ML. This form of declaration binds a list of identifiers to a type with associated operations, a composite "value" we call a data algebra. We use a second-order typed lambda calculus SOL to show how data algebras may be given types, passed as parameters, and returned as results of function calls. In the process, we discuss the semantics of abstract data type declarations and review a connection between typed programming languages and constructive logic.
ISSN:0164-0925
1558-4593
DOI:10.1145/44501.45065