Bohdan Liesnikov

At the moment I’m doing a PhD at TU Delft with Jesper Cockx. I’m working on dependently-typed programming languages, in particular on design and architecture of type-checkers and elaborators.

Sections on this page: Projects, Community, Links, Personal Details.

Projects

• Agda Core. With Jesper Cockx and Lucas Escot. In development. sources
• ExEl: building an elaborator using extensible constraints. With Jesper Cockx. IFL 2023. doi.org/10.1145/3652561.3652565, sources. A shorter (and outdated) TYPES version.
• Iris Proof Mode in Ltac2. Master's thesis with Derek Dreyer and Robbert Krebbers at University of Saarland. pdf and sources
• Generating induction principles and subterm relations for inductive types using MetaCoq. In collaboration with Marcel Ullrich and Yannick Forster. Coq Workshop 2020. pdf, sources1, and sources2.

Community

I've supervised a number of students while at TU Delft. Some MSc students: Jakob Naucke (ongoing), Ivar de Bruin, Paul van der Stel. And a few BSc students.

I helped design and run a FP course for BSc students at TU Delft, and during my time at Saarland I TA-ed Introduction to Computational Logic.

I've also been involved in bunch of meetups: co-organised FP Dag 2024, co-founded Papers We Love Kyiv, helped run and gave a talk at Kyiv::fprog.

Links

• Mastodon: @liesnikov@types.pl
• Github: github.com/@liesnikov
• Google Scholar: scholar.google.com/citations?user=9wjrYuMAAAAJ
• LinkedIn: linkedin.com/in/liesnikov/

Personal details

In professional circles I go by my full name: Bohdan Liesnikov. Outside of work I go by Dana. Pronouns: they/he.

If you'd like to contact me you can send a message on Mastodon or reach out via email: b dot mylastname at gmail.