Unifying Recursive and Co-recursive Definitions in Sheaf Categories

In this paper we present a theorem for defining fixed-points in categories of sheaves. This result gives a unifying and general account of most techniques used in computer science in order to ensure convergency of circular definitions, such as (but not limited to) well-founded recursion and contractivity in complete ultra metric spaces. This general fixed-point theorem encompasses also a similar set theoretic result presented in previous work, based on the notion of ordered family of equivalences, and implemented in the Coq proof assistant.

• Type: Conference
• Year: 2004
• Where: FOSSACS
• Authors: Pietro Di Gianantonio, Marino Miculan
• Keywords: Coq Proof Assistant, FOSSACS 2004, General Fixed-point Theorem, Software Engineering, Ultra Metric Spaces