Publications

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
 Breaking the Loop: Recursive Proofs for Coinductive Predicates in Fibrations. Henning Basold. In Under Review, 2018. [ bib  .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  .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 ]
 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 ]
 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  http ]
Journals
 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 ]
 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 ]
 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 ]
Theses
Short Contributions
 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  .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 ]
 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 ]
 A Note on Typed Behavioural Differential Equations. Henning Basold, Helle H. Hansen, and Jan J. M. M. Rutten. In CMCS Short Contributions, 2014. [ 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 ]
 Algebraic Characterisations of Signal Flow Graphs. Henning Basold, Marcello Bonsangue, and Jan Rutten. In CALCO Early Ideas, 2013. [ bib  .pdf ]