The Category-Theoretic Solution of Recursive Domain Equations
From MaRDI portal
Publication:3956379
DOI10.1137/0211062zbMath0493.68022OpenAlexW2024873396WikidataQ56486107 ScholiaQ56486107MaRDI QIDQ3956379
Gordon D. Plotkin, Michael B. Smyth
Publication date: 1982
Published in: SIAM Journal on Computing (Search for Journal in Brave)
Full work available at URL: http://wrap.warwick.ac.uk/46312/1/WRAP_Smyth_cs-rr-014.pdf
Semantics in the theory of computing (68Q55) Specification and verification (program logics, model checking, etc.) (68Q60) General topics in the theory of software (68N01)
Related Items
Computational adequacy via ‘mixed’ inductive definitions, A structural co-induction theorem, Coalgebraic Representation Theory of Fractals, The convex powerdomain in a category of posets realized by cpos, Universal domains and the amalgamation property, Least fixpoints of endofunctors of cartesian closed categories, Projections for polymorphic first-order strictness analysis, A domain equation for bisimulation, Unnamed Item, On Coalgebras over Algebras, From Coalgebraic to Monoidal Traces, Categorical data types in parametric polymorphism, Arrows of Times, Non Integer Operators, Self-Similar Structures, Zeta Functions and Riemann Hypothesis: a Synthetic Categorical Approach, Transport of finiteness structures and applications, Compositional characterization of observable program properties, An abstract interpretation for ML equality kinds, Fully abstract semantics for higher order communicating systems, A completeness theorem for nondeterministic Kleene algebras, Unnamed Item, Denotational semantics as a foundation for cost recurrence extraction for functional languages, From semantics to types: the case of the imperative \(\lambda\)-calculus, The glueing construction and lax limits, Unnamed Item, A generalization of the trie data structure, On systems of equations defining infinite graphs, Unnamed Item, The essence of ornaments, Unnamed Item, Call-by-name Gradual Type Theory, The Impact of the Lambda Calculus in Logic and Computer Science, Initial algebras and terminal coalgebras in many-sorted sets, A Coalgebraic View of Infinite Trees and Iteration, Towards Effects in Mathematical Operational Semantics, Realization of Coinductive Types, Fixed Points of Functors - A Short Abstract, Realisability semantics of parametric polymorphism, general references and recursive types, Kan injectivity in order-enriched categories, Type inference with simple subtypes, A Finite Axiomatization of Nondeterministic Regular Expressions, Recursive Domain Equations of Filter Models, Realizability Semantics of Parametric Polymorphism, General References, and Recursive Types, A categorical manifesto, Initial Algebra Semantics for Cyclic Sharing Structures, Extending set functors to generalised metric spaces, Algebraic specification of data types: A synthetic approach, Nested Hoare Triples and Frame Rules for Higher-Order Store, From term models to domains, Inversion, Iteration, and the Art of Dual Wielding, Unique, guarded fixed points in an additive setting, Logical Relations and Nondeterminism, A Convenient Category of Domains, The Bicategory-Theoretic Solution of Recursive Domain Equations, Syntactic Logical Relations for Polymorphic and Recursive Types, CPO-models for second order lambda calculus with recursive types and subtyping, Coalgebraic Trace Semantics for Combined Possibilitistic and Probabilistic Systems, Monads for behaviour, Banach's fixed-point theorem as a base for data-type equations, Merging regular processes by means of fixed-point theory, Weakly linear systems for matrices over the max-plus quantale, Towards a quantum domain theory: order-enrichment and fixpoints in \(W^*\)-algebras, Terminal coalgebras in well-founded set theory, Atomicity, coherence of information, and point-free structures, Parametrized fixed points and their applications to session types, Computational adequacy for recursive types in models of intuitionistic set theory, Universal profinite domains, Two-level semantics and code generation, A safe approach to parallel combinator reduction, Recursively defined domains and their induction principles, A principled approach to programming with nested types in Haskell, Substitution revisited, Semantics of higher-order quantum computation via geometry of interaction, 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, The connection between initial and unique solutions of domain equations in the partial order and metric approach, The contraction property is sufficient to guarantee the uniqueness of fixed points of endofunctors in a category of complete metric spaces, The category-theoretic solution of recursive metric-space equations, A characterization of distance between 1-bounded compact ultrametric spaces through a universal space, Equational properties of iteration in algebraically complete categories, \(\mathbb{T}^\omega\) as a universal domain, Least fixed point of a functor, The equational logic of fixed points, Trees and semantics, Approximating labelled Markov processes, On final coalgebras of continuous functors, A domain-theoretic semantics of lax generic functions., Infinite trees and completely iterative theories: A coalgebraic view, A fully abstract model for the \(\pi\)-calculus., Varieties of chain-complete algebras, A curry-style semantics of interaction: from untyped to second-order lazy \(\lambda\mu\)-calculus, Codatatypes in ML, Two-level semantics and abstract interpretation, On coalgebras over algebras, Free upper regular bands, A relational realizability model for higher-order stateful ADTs, Tree constructions of free continuous algebras, Non-deterministic information systems and their domains, Domain interpretations of Martin-Löf's partial type theory, Relatively terminal coalgebras, Sequential algorithms on concrete data structures, Towards a foundation for semantics in complete metric spaces, Recursion over realizability structures, Domain theory in logical form, Models of nondeterministic regular expressions, An irregular filter model, Universal homogeneous event structures and domains, Recursive types for Fun, On minimal coalgebras, Quantitative domains and infinitary algebras, Piecewise initial algebra semantics, Elements of generalized ultrametric domain theory, On the greatest fixed point of a set functor, A fixed-point theorem in a category of compact metric spaces, New foundations for fixpoint computations: FIX-hyperdoctrines and the FIX-logic, Strictness analysis via abstract interpretation for recursively defined types, Complete restrictions of the intersection type discipline, On Kan-injectivity of locales and spaces, Some economic applications of Scott domains, Tail recursion through universal invariants, I-categories as a framework for solving domain equations, The mixed powerdomain, Communicating processes with value-passing and assignments, Approximation in quantale-enriched categories, Algebraically compact functors, Simulations in coalgebra, Domain theory, testing and simulation for labelled Markov processes, Fixed-point constructions in order-enriched categories, Categories of embeddings, Categorical fixed point semantics, Infinite hypergraphs. I: Basic properties, Solving reflexive domain equations in a category of complete metric spaces, Functorial polymorphism, Notions of computation and monads, Non-well-founded sets modeled as ideal fixed points, Induction and recursion on the partial real line with applications to Real PCF, On functions preserving levels of approximation: A refined model construction for various lambda calculi, Structural induction and coinduction in a fibrational setting, Recursive domain equations for concrete data structure, Describing semantic domains with sprouts, Domain theoretic models of polymorphism, Equational logic of circular data type specification, Topology, domain theory and theoretical computer science, Universal coalgebra: A theory of systems, Structural operational semantics for continuous state stochastic transition systems, Games and full abstraction for FPC., On a generalized product for domains, Coalgebraic semantics for nominal automata, The genericity theorem and parametricity in the polymorphic \(\lambda\)- calculus, Set-theoretical and other elementary models of the \(\lambda\)-calculus, The generic approximation lemma, CSP, partial automata, and coalgebras., A co-induction principle for recursively defined domains, Polymorphic lambda calculus and subtyping., Fixpoint operators for domain equations, The comparison of a cpo-based semantics with a cms-based semantics for \(CSP\), Information categories
