The main research interests of Henning Basold are the study of logic and behaviour of systems, and the construction of calculi that allow us to formally describe and reason about various systems.

More information about Henning Basold

Some keywords that appear in Henning's research: Logic, category theory, coalgebra and coinduction, proof theory, type theory, programming languages, semantics, and computational models, concurrency, formally verified mathematics and programming, proof assistants, proofs-as-programs/Curry-Howard/Brouwer-Heyting-Kolmogorov interpretation, (co)homological algebra, mathematical biology.

Systems are an assemblage of objects or components that are interrelated. This concept occurs throughout computer science, mathematics, biology, physics and many other fields. Concrete examples of systems that Henning studies are computational models like automata, concurrent processes and probabilistic processes, control and reactive systems, combinatorics and recurrence relations, dynamical systems, systems of interacting agents, and biological systems. The main mathematical tools that he uses are coalgebras, coinduction, category theory, logic and type theory, with a particular focus on computer-verifiable correctness of proofs and programs.

Henning's research interest descend from the general desire to prevent errors in software, hardware, and mathematical or other theories, and to understand relations between different scientific fields. The approach chosen by Henning is the formalisation of artefacts, like software or theories, in terms of a syntactic logic, as a program, in a type theory or any other suitable syntactic language. A formal syntactic specification will allow then a computer to verify the correctness of behaviour and proofs. Leaving the creative work of building programs, models and proofs to humans and the mechanical work of verifying them to computers ensures not only correctness of artefacts and scales to arbitrary sizes, but it also frees us a from worries and allows us to focus on the interesting part of work as a programmer, mathematician, and biologist.

Short biography

Henning joined the theory group of LIACS mid-2019. Before that, he was a post-doc in the PLUME group of the Laboratoire de l'informatique du parallélisme at the ENS Lyon. He obtained his doctoral degree with the topic "Mixed Inductive-Coinductive Reasoning" under the supervision of Herman Geuvers, Helle Hvid Hansen and Jan Rutten at the Radboud University in collaboration with the CWI Amsterdam. The topics of Henning's bachelor and master's degree obtained at the TU Braunschweig were, respectively, elliptic curve cryptography on FPGAs and SMT-based verification of reactive systems written in ANSYS SCADE.