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

categorical semantics of computationscorrectnessfixpoint computationsfixpoint inductionhigher-order typed constructive predicate logicmonad

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40) Higher-type and set recursion theory (03D65) Proof theory and constructive mathematics (03F99) 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)

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

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

Cited in

(13)

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

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)