Henning Basold

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 Under Review, Nov 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 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.

Breaking the Loop — Recursive Proofs for Coinductive Predicates in Fibrations.
Henning Basold. In arXiv, Jan 2018. [ bib | pdf | arXiv ]

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 up-to techniques. This approach lifts the burden to guess invariants, like bisimulation relations, beforehand. Rather, they allow one to start with the sought-after 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 - Leibniz-Zentrum 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 327--336. 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 91--109, 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 3--17. Open Publishing Association, 2015. [ bib | DOI | .pdf ]
 
An Open Alternative for SMT-Based 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 124--139, 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 1--29, 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 ]
 
Well-Definedness and Observational Equivalence for Inductive-Coinductive 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 124--145, 2014. [ bib | DOI | .pdf ]

Pre-Prints

 
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 e-prints, February 2018. [ bib | arXiv | .pdf ]
 
Dependent Inductive and Coinductive Types via Dialgebras in Fibrations. Henning Basold. In Unpublished, April 2015. [ bib | .pdf ]

Theses

 
Mixed Inductive-Coinductive Reasoning: Types, Programs and Logic. Henning Basold. PhD Thesis, Radboud University, 2018. [ bib | http ]
 
Transformation von Scade-Modellen zur SMT-basierten 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 Inductive-Coinductive Logic Programs. Henning Basold and Ekaterina Komendantskaya. In Pre-Proceedings 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 ]
 
Dialgebra-Inspired 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 ]