Henning Basold

About Me

At my PhD defence

I am a lecturer (= assistant professor) at the Leiden Institute for Advanced Computer Science (LIACS) at the Universteit Leiden.

Before that, I was a postdoc with Damien Pous in the the PLUME team and a member of the CoVeCe project. My PhD thesis I wrote under the supervision of Helle Hvid Hansen, Jan Rutten and Herman Geuvers at the Radboud University, Nijmegen.

Research Interest

I am fascinated by the elegance that coalgebras and coinduction offer in understanding state-based systems, infinite structures and logical operations. Combining this with the beauty of automatically verifiable proofs obtained from type theory gives a rough idea of my research area.

News

TEASE-LP Started!.

Our workshop on Trends, Extensions, Applications and Semantics of Logic Programming (TEASE-LP) has started! We have a nice programme with pre-recorded lightning talks and two live sessions, supported by discussions. If you would like to join, please sign up in the discussion board.

Teaching PhD Position in Quantitative Systems and Reasoning Methods.

I have a fully funded PhD position at the Leiden University available with a rather free choice of approaching reasoning methods for quantitative systems. The approach can be purely in terms of category theory, type theory, formal logic, or a combination of those. Please note that the application deadline is 26 April 2020, but applications are accepted until the position is filled. More information about the research project and the details of the position can be found here. For further questions, please contact me.

Workshop for John Power.

I had the honour of attending the workshop on the occasion of John Power’s retirement in Bath. This was great meeting with some great people. Very refreshing to talk just about science and deep problems! Katya and I gave a joint talk, where she took care of the entertaining part with anecdotes and some history of her work with John, while I did the not-so-fun technical part about CUP and Garlic. The slides are here. Thank you Guy and Neil for this great workshop, all the best to you John in your new-won life in Australia!

Conferences and Visits in June 2019.

I was very happy to present my work at CALCO and MFPS this year in London. At CALCO, I introduced my Coinduction in Flow paper. For MFPS I was invited by Matteo Mio to give an introduction to the probabilistic programming language example in the same paper. Afterwards, we headed for TYPES in Oslo, where I talked about our recent work with Niels and Niccolò on free algrebras for algebraic theories as higher inductive types. The atmosphere at both events was great as always!

Coinduction in Flow — The Later Modality in Fibrations.
Henning Basold. In arXiv, Apr 2019. [ bib | pdf | arXiv ]

It is finally done! After a long time of improvement, I’m very pleased to announce that my paper on guarded recursion in fibrations has now been accepted at CALCO’19! [More...]

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.