A Calculus of Circular Proofs and its Categorical Semantics

Luigi Santocanale


We present a calculus of proofs, the intended models of which
are categories with finite products and coproducts, initial algebras
and final coalgebras of functors that are recursively constructible
out of these operations, that is, mu-bicomplete categories. The
calculus satisfies the cut elimination and its main characteristic is
that the underlying graph of a proof is allowed to contain a
certain amount of cycles. To each proof of the calculus we associate
a system of equations which has a meaning in every mu-bicomplete
category. We prove that this system admits always a unique
solution, and by means of this theorem we define the semantics of
the calculus.

Keywords: Initial algebras, final coalgebras. Fixed point calculi, mu-calculi.
Bicompletion of categories. Models of interactive computation.

Full Text:


DOI: http://dx.doi.org/10.7146/brics.v8i15.20472
This website uses cookies to allow us to see how the site is used. The cookies cannot identify you or any content at your own computer.

ISSN: 0909-0878 

Hosted by the Royal Danish Library and Aarhus University Library