Affiliations: [a] Dipartimento di Scienze Matematiche Informatiche e Fisiche Università di Udine via delle Scienze 206, I-33100 Udine, Italy fabio.alessi@uniud.it | [b] Dipartimento di Informatica, Università di Torino corso Svizzera 185 I-10149 Torino, Italy felice.cardone@unito.it
Correspondence:
[*]
Address for correspondence: Dipartimento di Informatica, Università di Torino, corso Svizzera 185 I-10149 Torino, Italy
Abstract: We investigate the foundations of reasoning over infinite data structures by means of set-theoretical structures arising in the sheaf-theoretic semantics of higher-order intuitionistic logic. Our approach focuses on a natural notion of tiering involving an operation of restriction of elements to levels forming a complete Heyting algebra. We relate these tiered objects to final coalgebras and initial algebras of a wide class of endofunctors of the category of sets, and study their order and convergence properties. As a sample application, we derive a general proof principle for tiered objects.
Keywords: complete Heyting algebras, sheaves, initial algebras, final coalgebras, infinite data structures, approximation lemma
