| 2026 | FSCD | A Bounded Parallel Intersection Type System. | Andrej Dudenhefner, Aleksy Schubert, Jakob Rehof |
| 2025 | FSCD | Mechanized Undecidability of Higher-Order Beta-Matching. | Andrej Dudenhefner |
| 2024 | FSCD | Mechanized Subject Expansion in Uniform Intersection Types for Perpetual Reductions. | Andrej Dudenhefner, Daniele Pautasso |
| 2022 | CSL | Constructive Many-One Reduction from the Halting Problem to Semi-Unification. | Andrej Dudenhefner |
| 2022 | FSCD | Certified Decision Procedures for Two-Counter Machines. | Andrej Dudenhefner |
| 2022 | ITP | Undecidability of Dyadic First-Order Logic in Coq. | Johannes Hostert, Andrej Dudenhefner, Dominik Kirst |
| 2021 | LICS | The Undecidability of System F Typability and Type Checking for Reductionists. | Andrej Dudenhefner |
| 2020 | FSCD | Undecidability of Semi-Unification on a Napkin. | Andrej Dudenhefner |
| 2017 | LICS | Typability in bounded dimension. | Andrej Dudenhefner, Jakob Rehof |
| 2017 | POPL | Intersection type calculi of bounded dimension. | Andrej Dudenhefner, Jakob Rehof |
| 2016 | ISoLA | Combinatory Process Synthesis. | Jan Bessai, Andrej Dudenhefner, Boris Ddder, Moritz Martens, Jakob Rehof |
| 2014 | ISoLA | Combinatory Logic Synthesizer. | Jan Bessai, Andrej Dudenhefner, Boris Ddder, Moritz Martens, Jakob Rehof |