Constructive versions of Tarski's fixed point theorems
From MaRDI portal
Publication:1260047
DOI10.2140/pjm.1979.82.43zbMath0413.06004OpenAlexW2087403174MaRDI QIDQ1260047
Publication date: 1979
Published in: Pacific Journal of Mathematics (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.2140/pjm.1979.82.43
monotone operatorcomplete latticecommuting operatorspreclosure operatorstationary transfinite iteration sequencesTarski's fixed point theorems
Related Items (81)
Coinductive predicates and final sequences in a fibration ⋮ Correctness of fixpoint transformations ⋮ Relating Coalgebraic Notions of Bisimulation ⋮ Computing Program Reliability Using Forward-Backward Precondition Analysis and Model Counting ⋮ An integer static analysis for better extrapolation in Uppaal ⋮ Latticed \(k\)-induction with an application to probabilistic programs ⋮ A fixpoint theory for non-monotonic parallelism ⋮ Property preserving abstractions for the verification of concurrent systems ⋮ Weakly-relational shapes for numeric abstractions: Improved algorithms and proofs of correctness ⋮ Why does Astrée scale up? ⋮ Categorical fixed point calculus ⋮ Program verification with interacting analysis plugins ⋮ Deriving escape analysis by abstract interpretation ⋮ CONCEPTS ASSOCIATED TO CRITERIA: A METHOD FOR KNOWLEDGE PROCESSING FROM FUZZY CONTEXTS ⋮ Recent advances in program verification through computer algebra ⋮ Control of \((max, +)\)-linear systems minimizing delays ⋮ Size-based termination of higher-order rewriting ⋮ ABSTRACT INDUCTIVE AND CO-INDUCTIVE DEFINITIONS ⋮ Compositional characterization of observable program properties ⋮ On Fixpoint/Iteration/Variant Induction Principles for Proving Total Correctness of Programs with Denotational Semantics ⋮ Algorithms for non-linear and stochastic resource constrained shortest path ⋮ Termination of rewrite relations on \(\lambda\)-terms based on Girard's notion of reducibility ⋮ An abstract interpretation framework for genotype elimination algorithms ⋮ TASS: the toolkit for accurate scientific software ⋮ Properties of data flow frameworks: A unified model ⋮ A divide-and-conquer approach for analysing overlaid data structures ⋮ Bisimulation and simulation algorithms on probabilistic transition systems by abstract interpretation ⋮ Fixed point theorems and semantics: A folk tale ⋮ Program derivation with verified transformations — a case study ⋮ Grammar semantics, analysis and parsing by abstract interpretation ⋮ Magic-sets for localised analysis of Java bytecode ⋮ The two variable per inequality abstract domain ⋮ An abstract interpretation-based model for safety semantics ⋮ The complexity of Tarski's fixed point theorem ⋮ Calculational design of a regular model checker by abstract interpretation ⋮ Thompson aggregators, Scott continuous koopmans operators, and least fixed point theory ⋮ Unlocking of predicate: application to constructing a non-anticipating selection ⋮ Computing difference abstractions of linear equation systems ⋮ An array content static analysis based on non-contiguous partitions ⋮ A Case Study in Abstract Interpretation Based Program Transformation ⋮ The use of two relations in \( L\)-fuzzy contexts ⋮ Fuzzy logic programming reduced to reasoning with attribute implications ⋮ Viable set computation for hybrid systems ⋮ Unnamed Item ⋮ Existence and uniqueness of fixed point in partially ordered sets and applications to ordinary differential equations ⋮ The fixed-point theory of strictly causal functions ⋮ Verification and falsification of programs with loops using predicate abstraction ⋮ Making abstract models complete ⋮ Unnamed Item ⋮ Contractive mapping theorems in partially ordered sets and applications to ordinary differential equations ⋮ Transforming semantics by abstract interpretation ⋮ Static extensivity analysis for \(\lambda\)-definable functions over lattices ⋮ The study of the interval-valued contexts ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Transfinite sequences in the programmed iteration method ⋮ Property persistence in the situation calculus ⋮ Demand-driven interprocedural analysis for map-based abstract domains ⋮ Abstracting Nash equilibria of supermodular games ⋮ On the complexity of dataflow analysis of logic programs ⋮ Unnamed Item ⋮ Bi-inductive structural semantics ⋮ Static analysis of arithmetical congruences ⋮ Coinductive predicates and final sequences in a fibration ⋮ Algorithms for the fixed point property ⋮ HOMOGENEITY AND FIX-POINTS: GOING FORTH! ⋮ Concept lattices defined from implication operators ⋮ Construction of the \(L\)-fuzzy concept lattice ⋮ Fixed points and coincidences of families of mappings between ordered sets and some metrical consequences ⋮ CONTEXTS WITH MULTIPLE WEIGHTED VALUES ⋮ Parsing as abstract interpretation of grammar semantics ⋮ An abstract interpretation framework to reason on finite failure and other properties of finite and infinite computations. ⋮ Closures and fairness in the semantics of programming logic ⋮ A general framework for types in graph rewriting ⋮ Down and up operators associated to fuzzy relations and t-norms: A definition of fuzzy semi-ideals ⋮ Constructive design of a hierarchy of semantics of a transition system by abstract interpretation ⋮ A proof of Tarski's fixed point theorem by application of Galois connections ⋮ A Decision Procedure for Guarded Separation Logic Complete Entailment Checking for Separation Logic with Inductive Definitions ⋮ An NSF proposal ⋮ Frameworks for abstract interpretation ⋮ Unresolved systems of language equations: expressive power and decision problems
This page was built for publication: Constructive versions of Tarski's fixed point theorems
