It is finally done! After a long time of improvement, I’m very pleased to announce that my paper on guarded recursion in fibrations has now been accepted at CALCO’19!

This paper provides a construction on fibrations that gives access to the so-called later modality, which allows for a controlled form of recursion in coinductive proofs and programs. The construction is essentially a generalisation of the topos of trees from the codomain fibration over sets to arbitrary fibrations. As a result, we obtain a framework that allows the addition of a recursion principle for coinduction to rather arbitrary logics and programming languages. The main interest of using recursion is that it allows one to write proofs and programs in a goal-oriented fashion. This allows for easily understandable coinductive proofs and programs, and fosters automatic proof search.

Part of the framework are also various results that enable a wide range of applications: preservation of (co)limits, exponentials, fibred adjunctions and first-order fibrations, which means that the construction extends any first-order logic with the later modality; soundness and completeness; and up-to techniques as proof rules. Since the construction works for a wide variety of fibrations, we will be able to use the recursion offered by the later modality in various context. In particular, we will show how recursive proofs can be obtained for arbitrary (syntactic) first-order logics, for coinductive set-predicates, and for the probabilistic modal $\mu$-calculus. Moreover, we use the same construction to obtain a novel language for probabilistic productive coinductive programming. These examples demonstrate the flexibility of the framework and its accompanying results.

Motivation for the Paper

The original motivation for writing this paper was to give an account to the logic that is developed in chapter 5 of my thesis. As it turned out, much of the syntactic development in my thesis could be hidden, if one instead works with fibrations. Such an approach requires some closure properties of fibrations that we construct in course of the paper. Among them is the Cartesian closure, which can be obtained as a certain limit construction (via so-called ends). This construction is on an abstract level quite intricate but, fortunately, it reduces in many cases to simple constructions that are well-known. In any case, on of the instances of the framework is the logic that I developed by hand in my thesis, albeit presented in a different form (sequences of first-order formulas instead of formulas in a logic enriched with the later modality). This presentation can be rectified though, thus a lot of the pedestrian work in my thesis is subsumed by this paper.