Breaking the Loop — Recursive Proofs for Coinductive Predicates in Fibrations. Henning Basold. In Under Review, Jan 2018. [ bib | pdf ]

The purpose of this paper is to develop and study recursive proofs of coinductive predicates in fibrations. Such recursive proofs allow one to discover proof goals in the construction of a proof of a coinductive predicate, while still allowing the use of up-to techniques. This approach lifts the burden to guess invariants, like bisimulation relations, beforehand. Rather, they allow one to start with the sought-after proof goal and develop the proof from there until a point is reached, at which the proof can be closed through a recursion step. Proofs given in this way are both easier to construct and to understand, similarly to proofs given in cyclic proof systems or by appealing parameterised coinduction. [Continue reading.]

Full List of Publications