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.

Projects

• Caching constraints in type-checkers. Shelved for the moment, sources for some of the experiments and slides from AIM XXXIX.
• Building A Correct-By-Construction Type Checker for a Dependently Typed Core Language. With Jesper Cockx at APLAS 2024. doi: 10.1007/978-981-97-8943-6_4, sources
• ExEl: building an elaborator using extensible constraints. With Jesper Cockx at IFL 2023. doi: 10.1145/3652561.3652565, sources. There is also a shorter (and outdated) TYPES abstract.
• 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: José Carlos Padilla Cancio (ongoing), Jakob Naucke, 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.