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

DOI10.1016/0890-5401(92)90018-BMaRDI QIDQ1193588zbMATH OpenOpenAlexFDO

Authors 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

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

Mathematics Subject Classification ID

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

Recommendations

• Computational adequacy of the FIX-logic
• Computational types from a logical perspective
• Publication:4206923
• On fixpoint objects and gluing constructions
• scientific article; zbMATH DE number 1678378

Cites work

• scientific article; zbMATH DE number 4179333 (Why is no real title available?)
• scientific article; zbMATH DE number 4048997 (Why is no real title available?)
• scientific article; zbMATH DE number 19484 (Why is no real title available?)
• scientific article; zbMATH DE number 42059 (Why is no real title available?)
• scientific article; zbMATH DE number 48157 (Why is no real title available?)
• scientific article; zbMATH DE number 50149 (Why is no real title available?)
• scientific article; zbMATH DE number 130889 (Why is no real title available?)
• scientific article; zbMATH DE number 193320 (Why is no real title available?)
• scientific article; zbMATH DE number 3557754 (Why is no real title available?)
• scientific article; zbMATH DE number 3367095 (Why is no real title available?)
• A type-theoretical alternative to ISWIM, CUCH, OWHY
• Algebraic specification of data types: A synthetic approach
• HYPERDOCTRINES, NATURAL DEDUCTION AND THE BECK CONDITION
• LCF considered as a programming language
• Logic and Computation
• Notions of computation and monads
• The Category-Theoretic Solution of Recursive Domain Equations
• The calculus of constructions

Cited in

(13)

• scientific article; zbMATH DE number 29052 (Why is no real title available?)
• Logical relations for monadic types
• Notions of computation and monads
• Structural induction and coinduction in a fibrational setting
• Deriving logical relations from interpretations of predicate logic
• Encoding FIX in Object Calculi
• On fixpoint objects and gluing constructions
• Axioms and (counter)examples in synthetic domain theory
• Interleaving data and effects
• Computational adequacy of the FIX-logic
• Traced Premonoidal Categories
• Intuitionistic fixed point logic
• A Semantical Approach to Equilibria and Rationality

This page was built for publication: New foundations for fixpoint computations: FIX-hyperdoctrines and the FIX-logic

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1193588)