1988/07/01 by John C. Mitchell, Gordon Plotkin · 4 citations
Computer Science · #Logic, programming, and type systems #Formal Methods in Verification #Software Engineering Research
paper · pdf · doi:10.1145/44501.45065
openalex publication_date 1988/07/01 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/14
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.