New foundations for fixpoint computations: FIX-hyperdoctrines and the FIX-logic

DOI10.1016/0890-5401(92)90018-BzbMath0763.03031OpenAlexW1977260399MaRDI QIDQ1193588

Roy L. Crole, Andrew M. Pitts

Publication date: 27 September 1992

Published in: Information and Computation (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/0890-5401(92)90018-b

zbMATH Keywords

correctnessmonadfixpoint inductioncategorical semantics of computationsfixpoint computationshigher-order typed constructive predicate logic

Mathematics Subject Classification ID

Semantics in the theory of computing (68Q55) Closed categories (closed monoidal and Cartesian closed categories, etc.) (18D15) Monads (= standard construction, triple or triad), algebras for monads, homology and derived functors for monads (18C15) Combinatory logic and lambda calculus (03B40) Higher-type and set recursion theory (03D65) Proof theory and constructive mathematics (03F99)

Related Items

A Semantical Approach to Equilibria and Rationality, Deriving logical relations from interpretations of predicate logic, Computational adequacy of the FIX-logic, On fixpoint objects and gluing constructions, Interleaving data and effects, Intuitionistic fixed point logic, Logical relations for monadic types, Unnamed Item, Notions of computation and monads, Traced Premonoidal Categories, Structural induction and coinduction in a fibrational setting, Axioms and (counter)examples in synthetic domain theory, Encoding FIX in Object Calculi

Cites Work

• Notions of computation and monads
• The calculus of constructions
• LCF considered as a programming language
• A type-theoretical alternative to ISWIM, CUCH, OWHY
• HYPERDOCTRINES, NATURAL DEDUCTION AND THE BECK CONDITION
• Logic and Computation
• Algebraic specification of data types: A synthetic approach
• The Category-Theoretic Solution of Recursive Domain Equations
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item