Data Types as Lattices

DOI10.1137/0205037zbMath0337.02018OpenAlexW4211265583MaRDI QIDQ4103509

Publication date: 1976

Published in: SIAM Journal on Computing (Search for Journal in Brave)

Full work available at URL: https://semanticscholar.org/paper/359eca57fe42d97cbb67f0b5591869abe5eb5421

Mathematics Subject Classification ID

Recursively (computably) enumerable sets and degrees (03D25) Combinatory logic and lambda calculus (03B40) Computability and recursion theory on ordinals, admissible sets, etc. (03D60)

Related Items

A domain-theoretic model of nominally-typed object-oriented programming, On merging software extensions, Infinite-word languages and continuous mappings, A characterization of F-complete type assignments, An algebraic semantics approach to the effective resolution of type equations, Universal profinite domains, Prime algebraicity, Two-level semantics and code generation, Testing equivalences for processes, Type theories, normal forms, and \(D_{\infty}\)-lambda-models, Polymorphic type inference and containment, A mathematical theory of randomized computation. I, A guided tour of the mathematics of MetaSoft '88, A small complete category, Innovations in computational type theory using Nuprl, On the uniqueness of fixed points of endofunctors in a category of complete metric spaces, On Church's formal theory of functions and functionals. The \(\lambda\)- calculus: Connections to higher type recursion theory, proof theory, category theory, Borel ideals vs. Borel sets of countable relations and trees, The contraction property is sufficient to guarantee the uniqueness of fixed points of endofunctors in a category of complete metric spaces, A decidable canonical representation of the compact elements in Scott's reflexive domain in \(P\omega\), Algebraic processing of programming languages, Enlargements of functional algebras for the lambda calculus, \(\mathbb{T}^\omega\) as a universal domain, The denotational semantics of sequential machines, Effectively given domains, Varieties of chain-complete algebras, Invertible terms in the lambda calculus, The Scott model of linear logic is the extensional collapse of its relational model, Petri nets, event structures and domains. I, Codatatypes in ML, Theory construction in psychology: The interpretation and integration of psychological data, Chain properties in Pomega, Recursion-closed algebraic theories, Two-level semantics and abstract interpretation, Free upper regular bands, A category-theoretic characterization of functional completeness, Tree constructions of free continuous algebras, An algebraic approach to stable domains, Graph grammars and operational semantics, Fixed point theorems and semantics: A folk tale, Towards a foundation for semantics in complete metric spaces, Recursion over realizability structures, Domain theory in logical form, An irregular filter model, Computability and the morphological complexity of some dynamics on continuous domains, Universal homogeneous event structures and domains, Rewrite, rewrite, rewrite, rewrite, rewrite, \dots, Sheaf toposes for realizability, Quantitative domains and infinitary algebras, Uniqueness of Scott's reflexive domain in \(P\omega \), Extremal solutions of inequations over lattices with applications to supervisory control, Lambda abstraction algebras: representation theorems, The category of equilogical spaces and the effective topos as homotopical quotients, Two models of synthetic domain theory, Strictness analysis via abstract interpretation for recursively defined types, On stable domains, CSP is a retract of CCS, Comparing free algebras in topological and classical domain theory, Computability in higher types, P\(\omega\) and the completeness of type assignment, Convex powerdomains. I, Categories of chain-complete posets, IO and OI. I, IO and OI. II, A theory of type polymorphism in programming, Data types, abstract data types and their specification problem, Fixed-point constructions in order-enriched categories, Operational domain theory and topology of sequential programming languages, Denotational semantics of an object-oriented programming language with explicit wrappers, Coherence and consistency in domains, The semantics of second-order lambda calculus, Functorial polymorphism, A note on complexity measures for inductive classes in constructive type theory, An algebraic generalization of Frege structures -- binding algebras, On combinatory algebras and their expansions, Expressive power of typed and type-free programming languages, A finite equational axiomatization of the functional algebras for the lambda calculus, Properly injective spaces and function spaces, Topology, domain theory and theoretical computer science, Set-theoretical models of lambda-calculus: theories, expansions, isomorphisms, Separately continuous algebras, Kleene chain completeness and fixedpoint properties, The insensitivity theorem for nonreducing reflexive types, Completeness of type assignment in continuous lambda models, Algebraic domain equations, Algebraic relations and presentations, Order completion monads, An effectively given initial semigroup, Rewrite systems on a lattice of types, Nominalization, predication and type containment, Computational foundations of basic recursive function theory, Set-theoretical and other elementary models of the \(\lambda\)-calculus, Using information systems to solve recursive domain equations, Closure functions and general iterates as reflectors, Admissible representations of effective cpo's, The comparison of a cpo-based semantics with a cms-based semantics for \(CSP\), A characterization of Plotkin's order in powerdomains, and some of its properties, Type 2 recursion theory, Theory of representations, Deductive and inductive synthesis of equational programs, An algebraic semantics of higher-order types with subtypes, Strong computable type, Expressing computational complexity in constructive type theory, From operational to denotational semantics, The order-K-ification monads, A process calculus for spiking neural P systems, Typed equivalence, type assignment, and type containment, The interpretation of unsolvable λ-terms in models of untyped λ-calculus, My ADT Shrine, A Cartesian closed category of domains with almost algebraic bases, Algebraic semantics and complexity of term rewriting systems, Trees from Functions as Processes, Linear time and branching time semantics for recursion with merge, Universal domains and the amalgamation property, Building domains from graph models, Rétractions et interprétation interne du polymorphisme : le problème de la rétraction universelle, Unnamed Item, Tree structure for distributive lattices and its applications, Unnamed Item, Constructive natural deduction and its ‘ω-set’ interpretation, Semantics of the second order lambda calculus, Unnamed Item, A class of bounded functions, a database language and an extended lambda calculus, Labelled reductions, runtime errors, and operational subsumption, Effective inseparability in a topological setting, Unnamed Item, Unified Algebras and action semantics, Higher-order order-sorted algebras, An abstract interpretation for ML equality kinds, Full abstraction and the Context Lemma (preliminary report), Wrapper semantics of an object-oriented programming language with state, Equilogical spaces and algebras for a double-power monad, Triposes, exact completions, and Hilbert's \(\varepsilon\)-operator, The equational logic of fixed points, An algebraic theory for data linkage, Extensions of Scott's graph model and Kleene's second algebra, THE WADGE ORDER ON THE SCOTT DOMAIN IS NOT A WELL-QUASI-ORDER, Descriptive complexity of \(\mathsf{qc} \mathsf{b}_0\)-spaces, Splitting and nonsplitting in the \(\Sigma_2^0\) enumeration degrees, Categorical semantics for higher order polymorphic lambda calculus, A stable universal domain related to ^ω, Correctness of compiling polymorphism to dynamic typing, Tarski’s Influence on Computer Science, Call-by-name Gradual Type Theory, Unnamed Item, Verifying of interface assertions for infinite state Mealy machines, What is a universal higher-order programming language?, Unnamed Item, Logic and functional programming by retractions, State-transition machines for lambda-calculus expressions, Collapsing partial combinatory algebras, R n - and G n -logics, Assertions and recursions, Stochastic \(\lambda\)-calculi: an extended abstract, From Böhm's Theorem to Observational Equivalences, Towards Lambda Calculus Order-Incompleteness, Unnamed Item, Sobriety for equilogical spaces, Anatomy of a domain of continuous random variables. I, New perspectives of granular computing in relation geometry induced by pairings, Anatomy of a Domain of Continuous Random Variables II, Cartesian closed stable categories, On the ubiquity of certain total type structures, Type inference with simple subtypes, Universal Constructions for (Co)Relations: categories, monoidal categories, and props, On the computational content of the Lawson topology, A type-theoretic semantics of arrays, Domains via graphs, Intersection types for \(\lambda\)-trees, On the construction of stable models of untyped \(\lambda\)-calculus, Lazy Lambda calculus: Theories, models and local structure characterization, On paradoxes in normal form, Unnamed Item, Set relations and set systems induced by some families of integral domains, Actors without Directors: A Kahnian View of Heterogeneous Systems, Unnamed Item, Three counterexamples concerning ω-chain completeness and fixed point properties, Can LCF be topped! Flat lattice models of typed \(\lambda{}\)-calculus, On Scott's thesis for domains of information and well-quasi-orderings, From parametric polymorphism to models of polymorphic FPC, Algebraic specification of data types: A synthetic approach, A unifying theorem for algebraic semantics and dynamic logics, From term models to domains, Continuously generated fixed points, Retracts of numerations, Equational logic of circular data type specification, Building continuous webbed models for system F, Dynamic game semantics, Characterizations of semantic domains for randomized algorithms, Meeting of the Association for Symbolic Logic, In Scott-Strachey style denotational semantics, parallelism implies nondeterminism, Unique, guarded fixed points in an additive setting, The completeness theorem for typing lambda-terms, From computation to foundations via functions and application: The \(\lambda\)-calculus and its webbed models, On the algebraic models of lambda calculus, Locally cartesian closed exact completions, The sequentially realizable functionals, Intersection and singleton type assignment characterizing finite Böhm-trees, An abstract approach to stratification in linear logic, Computability and realizability for interactive computations, StkTokens: Enforcing well-bracketed control flow and stack encapsulation using linear capabilities, Almost Every Domain is Universal, Meeting of the Association for Symbolic Logic Florence, Italy 1982, Definition of the semantics of programming language constructs in terms of ?-calculus. I, Resource traces: A domain for processes sharing exclusive resources., A coinductive completeness proof for the equivalence of recursive types