A Fibrational Method of Indexed Coinductive Data Types

摘要

As a fundamental issue in type theory, indexed coinductive data types (ICDT, for short) is of crucial importance, which is essentially semantic computing problem in programming. Based on fibrational method, this paper analyses semantic behaviours of ICDT and describes their universal coinductive rules. We executed some works in semantic computing and program logic of ICDT including their math structures and categorical properties. Example analyses prove the effectiveness of the proposed fibrational method and its applicability in program languages. Our work is based on fibration; a general math setting that can compute semantics automatically rather than depend on particular computing environments and syntactic forms of ICDT.