Indexed Coinduction in a Fibrational Setting

  • Decheng MiaoEmail author
  • Jianqing Xi
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 11338)


This paper provided some logical structures over fibration including comprehension and equation functor, then described semantic behavior by corecursion, also represented universal coinductive rule in a fibrational setting. Comparing the traditional methods, our works do not rely on special semantics computation context, which can analyze semantics elaborately of indexed coinductive data type and described its coinductive rule.


Semantic behavior Coinduction rule Fibration Lift Corecursion 



This study is supported by Guangdong Province High School Outstanding Young Teacher Training Project, China (Grant No. YQ2014155) and Guangdong Provincial Natural Science Foundation, China (Grant No. 2018A0303130274).


  1. 1.
    Greiner, J.: Programming with inductive and co-inductive types. School of Computer Science, Carnegie Mellon University, Pittsburgh, USA (1992)Google Scholar
  2. 2.
    Rutten, J.: Universal coalgebra: a theory of systems. Theor. Comput. Sci. 249(1), 3–80 (2000)MathSciNetCrossRefGoogle Scholar
  3. 3.
    Johnson, M., Rosebrugh, R., Wood, R.J.: Lenses, fibrations and universal translations. Math. Struct. Comput. Sci. 22, 25–42 (2012)MathSciNetCrossRefGoogle Scholar
  4. 4.
    Miao, D.C., Xi, J.Q., Jia, L.Y., et al.: Formal language algebraic model. J. South China Univ. Technol. (Nat. Sci. Ed.) 39(10), 74–78 (2011)Google Scholar
  5. 5.
    Hermida, C., Jacobs, B.: Structural induction and coinduction in a fibrational setting. Inf. Comput. 145(2), 107–152 (1998)MathSciNetCrossRefGoogle Scholar
  6. 6.
    Barr, M., Wells, C.: Category Theory for Computing Science. Prentice-Hall, NewYork (1990)zbMATHGoogle Scholar
  7. 7.
    Ghani, N., Johann, P., Fumex, C.: Indexed induction and coinduction, fibrationally. Log. Methods Comput. Sci. 9(3–6), 1–31 (2013)MathSciNetzbMATHGoogle Scholar

Copyright information

© Springer Nature Switzerland AG 2018

Authors and Affiliations

  1. 1.Shaoguan UniversityShaoguanChina
  2. 2.South China University of TechnologyGuangzhouChina

Personalised recommendations