Algebraic specification of data types: A synthetic approach

DOI10.1007/BF01752392zbMath0457.68035MaRDI QIDQ3907066

Michael B. Smyth, Daniel J. Lehmann

Publication date: 1981

Published in: Mathematical Systems Theory (Search for Journal in Brave)

zbMATH Keywords

implementationdata typedomain equationsinitialityfunction space constructor

Mathematics Subject Classification ID

Abstract data types; algebraic specification (68Q65) Data structures (68P05)

Related Items

μ-Bicomplete Categories and Parity Games ⋮ Semantic analysis of normalisation by evaluation for typed lambda calculus ⋮ A structural co-induction theorem ⋮ Parametrized fixed points and their applications to session types ⋮ Categorical fixed point calculus ⋮ Recursively defined domains and their induction principles ⋮ Algebraic solutions to recursion schemes ⋮ Categories, relations and dynamic programming ⋮ Categorical data types in parametric polymorphism ⋮ Equational properties of iteration in algebraically complete categories ⋮ Equational Properties of Fixed Point Operations in Cartesian Categories: An Overview ⋮ Unnamed Item ⋮ The equational logic of fixed points ⋮ On the algebra of order ⋮ On systems of equations defining infinite graphs ⋮ Codatatypes in ML ⋮ Two-level semantics and abstract interpretation ⋮ Interleaving data and effects ⋮ Graph grammars and operational semantics ⋮ Equational properties of fixed-point operations in cartesian categories: An overview ⋮ Unnamed Item ⋮ Generic functional programming with types and relations ⋮ Datatype laws without signatures ⋮ Fixed-point operations on ccc's. I ⋮ The meaning of specifications I: Domains and initial models ⋮ New foundations for fixpoint computations: FIX-hyperdoctrines and the FIX-logic ⋮ From Grammars and Automata to Algebras and Coalgebras ⋮ Some economic applications of Scott domains ⋮ Fusion of recursive programs with computational effects ⋮ Infinite hypergraphs. I: Basic properties ⋮ Induction and recursion on the partial real line with applications to Real PCF ⋮ Structural induction and coinduction in a fibrational setting ⋮ Equational logic of circular data type specification ⋮ From Parity Games to Circular Proofs ⋮ Unique, guarded fixed points in an additive setting ⋮ List Objects with Algebraic Structure ⋮ Universal coalgebra: A theory of systems ⋮ The Bicategory-Theoretic Solution of Recursive Domain Equations ⋮ CPO-models for second order lambda calculus with recursive types and subtyping

Uses Software

• ALGOL 68

Cites Work

• Effectively given domains
• Revised report on the algorithmic language ALGOL 68
• Categories of chain-complete posets
• Power domains
• Fixed-point constructions in order-enriched categories
• The Category-Theoretic Solution of Recursive Domain Equations
• Recursive data structures
• Data Types as Lattices
• A Powerdomain Construction
• Abstract data types and the development of data structures
• Initial Algebra Semantics and Continuous Algebras
• AN ELEMENTARY THEORY OF THE CATEGORY OF SETS
• Heterogeneous algebras
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item