Original scientific paper

https://doi.org/10.17559/TV-20191130092745

A Fibrational Method of Indexed Coinductive Data Types

Decheng Miao ; School of Information Science and Engineering, Shaoguan University, No. 288, Daxue Road, Zhenjiang District, Shaoguan, China
Chaoyang Wang ; School of Journalism and Communication, Guangzhou University, No. 230, Waihuanxi Road, Panyu District,Guangzhou, China
Xinsheng Liu ; Army Artillery and Air Defense Force Academy, No. 31, Dongdaying Road, Shenhe District, Shenyang, China
Yonglin Liang ; School of Information Science and Engineering, Shaoguan University, No. 288, Daxue Road, Zhenjiang District, Shaoguan, China

Abstract

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.

Keywords

category; coinductive data types; computation; fibration; programming

Hrčak ID:

236789

URI

https://hrcak.srce.hr/236789

Publication date:

15.4.2020.

Visits: 1.410 *