Henning Basold
Assistant professor
- Name
- Dr. H. Basold
- Telephone
- +31 71 527 6435
- h.basold@liacs.leidenuniv.nl
- ORCID iD
- 0000-0001-7610-8331
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
PhD Candidates
Publications
Links
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.
Assistant professor
- Science
- Leiden Inst of Advanced Computer Science
- Henning Basold (2019), Coinduction in Flow: The Later Modality in Fibrations. Roggenbach M. & Sokolova A. (Eds.), 8th Conference on Algebra and Coalgebra in Computer Science (CALCO 2019). 8th Conference on Algebra and Coalgebra in Computer Science (CALCO 2019) 3 June 2019 - 6 June 2019 no. 139. Dagstuhl, Germany: Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik. 8:1--8:22.
- Basold Henning & Geuvers Herman (2016), Type Theory Based on Dependent Inductive and Coinductive Types, LICS '16: Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science•. LICS '16: 31st Annual ACM/IEEE Symposium on Logic in Computer Science 5 July 2016 - 8 July 2016. New York, NY, U.S.A.: ACM. 327-336.
- Basold Henning & Komendantskaya Ekaterina (2016), Models of inductive-coinductive logic programs. Komendantskaya E. & František F. (Eds.), Pre-Proceedings of the Workshop on Coalgebra, Horn Clause Logic Programming and Types (CoALP-Ty16). Workshop on Coalgebra, Horn Clause Logic Programming and Types, CoALP-Ty'16 28 November 2016 - 29 November 2016: EPTCS . 23-24.
- Basold H. (2015), Dependent Inductive and Coinductive Types Are Fibrational Dialgebras. Matthes R. & Mio M. (Eds.), Proceedings Tenth International Workshop on Fixed Points in Computer Science (FICS 2015). 10th International Workshop on Fixed Points in Computer Science 11 September 2015 - 12 September 2015 no. 191: Open Publishing Association. 3-17.
- Basold H., Günther H., Huhn M. & Milius S. (2014), An Open Alternative for SMT-Based Verification of Scade Models. Lang F. & Flammini F. (Eds.), Formal Methods for Industrial Critical Systems. FMICS 2014. International Workshop on Formal Methods for Industrial Critical Systems FMICS 2014 30 August 2014 - 31 August 2014 no. 8718. Cham: Springer. 124-139.