Publications
On this page, you may find my publications. For a full list, see below. 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 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 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 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.
Full List of Publications
Conferences
 Coinduction in Uniform: Foundations for Corecursive Proof Search with Horn Clauses. Henning Basold, Ekaterina Komendantskaya, and Yue Li. In ESOP'19, volume 11423 of LNCS. Springer, 2019. [ bib  arXiv  .pdf ]
 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  .pdf ]
 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  arXiv  .pdf ]
 Newton Series, Coinductively. Henning Basold, Helle Hvid Hansen, JeanÉric Pin, and Jan Rutten. In Proceedings of ICTAC '15, pages 91109, 2015. [ bib  DOI  .pdf ]
 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  .pdf ]
 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  .pdf ]
Journals
 Newton Series, Coinductively: A Comparative Study of Composition. Henning Basold, Helle Hvid Hansen, JeanÉric Pin, and Jan Rutten. MSCS, pages 129, 2017. [ bib  DOI  .pdf ]
 Higher Inductive Types in Programming. Henning Basold, Herman Geuvers, and Niels van der Weide. J.UCS, David Turner's Festschrift  Functional Programming: Past, Present, and Future, 2017. [ bib  http ]
 WellDefinedness and Observational Equivalence for InductiveCoinductive Programs. Henning Basold and Helle Hvid Hansen. J. Log. Comput., April 2016. [ bib  DOI  .pdf ]
 Type Theory Based on Dependent Inductive and Coinductive Types. Henning Basold and Herman Geuvers. CoRR, abs/1605.02206, 2016. [ bib  http ]
 (Co)Algebraic Characterizations of Signal Flow Graphs. Henning Basold, Marcello 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 ]
Theses
 Mixed InductiveCoinductive Reasoning: Types, Programs and Logic. Henning Basold. PhD Thesis, Radboud University, 2018. [ bib  http ]
 Transformation von ScadeModellen zur SMTbasierten Verifikation. Henning Basold. Master's Thesis, TU Braunschweig, October 2012. [ bib  arXiv  http ]
 Parallelism Investigation for Elliptic Curve Key Exchange. Henning Basold. Bachelor's Thesis, TU Braunschweig, November 2010. [ 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 ]