Publications

Coinduction in Flow — The Later Modality in Fibrations.

Henning Basold. In arXiv, Apr 2019. [ bib | pdf | arXiv ]

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. [Continue reading.]

Coinduction in Uniform — Foundations for Corecursive Proof Search with Horn Clauses.

Henning Basold, Ekaterina Komendantskaya, and Yue Li. In ESOP 2019, Apr 2019. [ bib | pdf | arXiv ]

In this paper, we develop uniform proofs à la Miller and Nadathur for coinductive predicates in 8 different logics that vary in expressive power. Such proofs allow algorithmic proof search, as the application of proof rules is deterministic for each connective. We show that these uniform proofs are sound relative to an intuitionistic first-order logic with recursion that was proposed here. Moreover, we show that both proof systems are sound with respect to complete Herbrand models. This proof is presented in a modern, coalgebraic style. Finally, we provide heuristics for the discovery of proof goals, which is necessary to answer certain queries that arise from Horn clause programming. Such a discovery is necessary, as the original query can often not be proven directly but needs to be strengthened first.

Full List of Publications