Projects per year
Abstract
This paper extends the fibrational approach to induction and coinduction pioneered by Hermida and Jacobs, and developed by the current authors, in two key directions. First, we present a sound coinduction rule for any data type arising as the final coalgebra of a functor, thus relaxing Hermida and Jacobs’ restriction to polynomial data types. For this we introduce the notion of a quotient category with equality (QCE), which both abstracts the standard notion of a fibration of relations constructed from a given fibration, and plays a role in the theory of coinduction dual to that of a comprehension category with unit (CCU) in the theory of induction. Second, we show that indexed inductive and coinductive types also admit sound induction and coinduction rules. Indexed data types often arise as initial algebras and final coalgebras of functors on slice categories, so our key technical results give sufficent conditions under which we can construct, from a CCU (QCE) U : E > B, a fibration with base B/I that models indexing by I and is also a CCU (QCE).
Original language  English 

Title of host publication  Algebra and coalgebra in computer science 
Subtitle of host publication  Proceedings of the 4th international conference, CALCO 2011, Winchester, UK, August 30  September 2, 2011 
Editors  Andrea Corradini, Bartek Klin, Corina Cirstea 
Publisher  Springer 
Pages  176191 
Number of pages  15 
ISBN (Print)  9783642229435 
Publication status  Published  2011 
Publication series
Name  Lecture Notes in Computer Science 

Publisher  Springer 
Volume  6859 
ISSN (Print)  03029743 
Keywords
 automata theory
 reversible processes
 duality
 computational logic
 coalgebraic semantics
 coalgebraic logics
 categories
Fingerprint Dive into the research topics of 'Indexed induction and coinduction, fibrationally.'. Together they form a unique fingerprint.
Projects
 1 Finished

Categorical Foundations of Indexed Programming
Johann, P. & Ghani, N.
EPSRC (Engineering and Physical Sciences Research Council)
1/07/09 → 31/12/12
Project: Research