Dual unbounded nondeterminacy, recursion, and fixpoints

DOI10.1007/s00236-007-0049-9zbMath1127.68018MaRDI QIDQ995749

Joseph M. Morris, Malcolm Tyrrell

Publication date: 10 September 2007

Published in: Acta Informatica (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s00236-007-0049-9

Mathematics Subject Classification ID

68N18: Functional programming and lambda calculus

68Q60: Specification and verification (program logics, model checking, etc.)

Related Items

Modelling higher-order dual nondeterminacy, Alternating states for dual nondeterminism in imperative programming

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• A theoretical basis for stepwise refinement and the programming calculus
• Fixed-point calculus
• The Hoare and Symth power domain constructors commute under composition
• Duality in specification languages: A lattice-theoretical approach
• The free completely distributive lattice over a poset
• A theory for nondeterminism, parallelism, communication, and concurrency
• Predicate-transformer semantics of general recursion
• Interpretations of recursion under unbounded nondeterminacy
• Lower and upper power domain constructions commute on all cpos
• Power domain constructions
• Power domains
• Nondeterminacy and recursion via stacks and games
• A source of inconsistency in theories of nondeterministic functions
• A fixpoint theory for non-monotonic parallelism
• General correctness: A unification of partial and total correctness
• A lattice-theoretical fixpoint theorem and its applications
• Countable nondeterminism and random assignment
• A Powerdomain Construction
• Mathematics of Program Construction