Abstract
This paper provides a construction on fibrations that gives access to the socalled 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 goaloriented fashion. This enables 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: transportation of (co)limits, exponentials, fibred adjunctions and firstorder connectives from the initial fibration to the one constructed through the framework. This means that the framework extends any firstorder logic with the later modality. Moreover, we obtain soundness and completeness results, and can use upto 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. For instance, we will show how recursive proofs can be obtained for arbitrary (syntactic) firstorder logics, for coinductive setpredicates, and for the probabilistic modal mucalculus. Finally, 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.
BibTeX  Entry
@InProceedings{basold:LIPIcs:2019:11436,
author = {Henning Basold},
title = {{Coinduction in Flow: The Later Modality in Fibrations}},
booktitle = {8th Conference on Algebra and Coalgebra in Computer Science (CALCO 2019)},
pages = {8:18:22},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {9783959771207},
ISSN = {18688969},
year = {2019},
volume = {139},
editor = {Markus Roggenbach and Ana Sokolova},
publisher = {Schloss DagstuhlLeibnizZentrum fuer Informatik},
address = {Dagstuhl, Germany},
URL = {http://drops.dagstuhl.de/opus/volltexte/2019/11436},
URN = {urn:nbn:de:0030drops114369},
doi = {10.4230/LIPIcs.CALCO.2019.8},
annote = {Keywords: Coinduction, Fibrations, Later Modality, Recursive Proofs, Upto techniques, Probabilistic Logic, Probabilistic Programming}
}
Keywords: 

Coinduction, Fibrations, Later Modality, Recursive Proofs, Upto techniques, Probabilistic Logic, Probabilistic Programming 
Collection: 

8th Conference on Algebra and Coalgebra in Computer Science (CALCO 2019) 
Issue Date: 

2019 
Date of publication: 

25.11.2019 