Generating induction principles and subterm relations for inductive types using MetaCoq. - Bohdan Liesnikov; Marcel Ullrich; Yannick Forster 002 (CoRR, 2020)

ExEl: Building an Elaborator Using Extensible Constraints. - Bohdan Liesnikov; Jesper Cockx (IFL, 2023)

Building a Correct-by-Construction Type Checker for a Dependently Typed Core Language. - Bohdan Liesnikov; Jesper Cockx (APLAS, 2024)