Publications
On this page, you may find my publications. For a full list, see below. Coinduction in Uniform — Foundations for Corecursive Proof Search with Horn Clauses.

Henning Basold, Ekaterina Komendantskaya, and Yue Li.
In In Progress, Aug 2018.
[
bib
 pdf
]
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 firstorder 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.
 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 upto techniques. This approach lifts the burden to guess invariants, like bisimulation relations, beforehand. Rather, they allow one to start with the soughtafter 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
Conferences
 Monoidal Company for Accessible Functors. Henning Basold, Damien Pous, and Jurriaan Rot. In CALCO 2017, volume 72 of LIPIcs. Schloss Dagstuhl  LeibnizZentrum fuer Informatik, 2017. [ bib  DOI ]
 Type Theory Based on Dependent Inductive and Coinductive Types. Henning Basold and Herman Geuvers. In Proceedings of LICS '16, pages 327336. ACM, 2016. [ bib  DOI ]
 Newton Series, Coinductively. Henning Basold, Helle Hvid Hansen, JeanÉric Pin, and Jan Rutten. In Proceedings of ICTAC '15, pages 91109, 2015. [ bib  DOI ]
 Dependent Inductive and Coinductive Types Are Fibrational Dialgebras. Henning Basold. In Ralph Matthes and Matteo Mio, editors, Proceedings of FICS '15, volume 191 of EPTCS, pages 317. Open Publishing Association, 2015. [ bib  DOI ]
 An Open Alternative for SMTBased Verification of Scade Models. Henning Basold, Henning Günther, Michaela Huhn, and Stefan Milius. In Proceedings of Formal Methods for Industrial Critical Systems, FMICS 2014, pages 124139, 2014. [ bib  DOI ]
Journals
 Newton Series, Coinductively: A Comparative Study of Composition. Henning Basold, Helle Hvid Hansen, JeanÉric Pin, and Jan Rutten. Special MSCS Issue of Best ICTAC 2015 Papers, To Appear, 2017. [ bib  .pdf ]
 Higher Inductive Types in Programming. Henning Basold, Herman Geuvers, and Niels van der Weide. Journal of Universal Computer Science, David Turner's Festschrift  Functional Programming: Past, Present, and Future, 2017. [ bib  .pdf ]
 WellDefinedness and Observational Equivalence for InductiveCoinductive Programs. Henning Basold and Helle Hvid Hansen. Journal of Logic and Computation, April 2016. [ bib  DOI  .pdf ]
 (Co)Algebraic Characterizations of Signal Flow Graphs. Henning Basold, Marcello M. Bonsangue, Helle Hvid Hansen, and Jan Rutten. In Horizons of the Mind  Prakash Panangaden Festschrift, pages 124145, 2014. [ bib  DOI  .pdf ]
Preprints
 Coinduction in Uniform: Foundations for Corecursive Proof Search with Horn Clauses. Henning Basold, Ekaterina Komendantskaya, and Yue Li. In Unpublished, July 2018. [ bib  .pdf ]
 Breaking the Loop: Recursive Proofs for Coinductive Predicates in Fibrations. Henning Basold. ArXiv eprints, February 2018. [ bib  arXiv  .pdf ]
 Dependent Inductive and Coinductive Types via Dialgebras in Fibrations. Henning Basold. In Unpublished, April 2015. [ bib  .pdf ]
Abstracts
 The Later Modality in Fibrations. Henning Basold. In Extended Abstracts for International Conference on Types for Proofs and Programs (TYPES), June 2018. [ bib ]
 Models of InductiveCoinductive Logic Programs. Henning Basold and Ekaterina Komendantskaya. In PreProceedings of the Workshop on Coalgebra, Horn Clause Logic Programming and Types, November 2016. [ bib  arXiv  .pdf ]
 Type Theory Based on Dependent Inductive and Coinductive Types. Henning Basold and Herman Geuvers. In Extended Abstracts for International Conference on Types for Proofs and Programs (TYPES), May 2016. [ bib  DOI ]
 Dependent Inductive and Coinductive Types Through Dialgebras in Fibrations. Henning Basold and Herman Geuvers. In Extended Abstracts for International Conference on Types for Proofs and Programs (TYPES), May 2015. [ bib  .pdf ]
 DialgebraInspired Syntax for Dependent Inductive and Coinductive Types. Henning Basold and Herman Geuvers. In Extended Abstracts for International Conference on Types for Proofs and Programs (TYPES), May 2015. [ bib  .pdf ]
 Observational Equivalence for Behavioural Differential Equations. Henning Basold and Helle Hvid Hansen. In Extendend Abstracts for the Workshop on Proof, Structures and Computation, 2014. [ bib  .pdf ]
 A Note on Typed Behavioural Differential Equations. Henning Basold, Helle H. Hansen, and Jan Rutten. In CMCS Short Contributions, 2014. [ bib  .pdf ]
 Algebraic Characterisations of Signal Flow Graphs. Henning Basold, Marcello Bonsangue, and Jan Rutten. In CALCO Early Ideas, 2013. [ bib  .pdf ]