Combinatory Logic Synthesizer. - Jan Bessai; Andrej Dudenhefner; Boris Düdder; Moritz Martens; Jakob Rehof (ISoLA (1), 2014)

Typing Classes and Mixins with Intersection Types. - Jan Bessai; Boris Düdder; Andrej Dudenhefner; Tzu-Chun Chen; Ugo de'Liguoro (ITRS, 2014)

Combinatory Process Synthesis. - Jan Bessai; Andrej Dudenhefner; Boris Düdder; Moritz Martens; Jakob Rehof (ISoLA (1), 2016)

The Intersection Type Unification Problem. - Andrej Dudenhefner; Moritz Martens; Jakob Rehof (FSCD, 2016)

Typability in bounded dimension. - Andrej Dudenhefner; Jakob Rehof (LICS, 2017)

Intersection type calculi of bounded dimension. - Andrej Dudenhefner; Jakob Rehof (POPL, 2017)

The Complexity of Principal Inhabitation. - Andrej Dudenhefner; Jakob Rehof (FSCD, 2017)

Lower End of the Linial-Post Spectrum. - Andrej Dudenhefner; Jakob Rehof (TYPES, 2017)

Rank 3 Inhabitation of Intersection Types Revisited (Extended Version). - Andrej Dudenhefner; Jakob Rehof (CoRR, 2017)

The Algebraic Intersection Type Unification Problem. - Andrej Dudenhefner; Moritz Martens; Jakob Rehof (Log. Methods Comput. Sci., 2017)

A Simpler Undecidability Proof for System F Inhabitation. - Andrej Dudenhefner; Jakob Rehof (TYPES, 2018)

Mixin Composition Synthesis based on Intersection Types. - Jan Bessai; Tzu-Chun Chen; Andrej Dudenhefner; Boris Düdder; Ugo de'Liguoro; Jakob Rehof (Log. Methods Comput. Sci., 2018)

Undecidability of Intersection Type Inhabitation at Rank 3 and its Formalization. - Andrej Dudenhefner; Jakob Rehof (Fundam. Informaticae, 2019)

Principality and approximation under dimensional bound. - Andrej Dudenhefner; Jakob Rehof (Proc. ACM Program. Lang., 2019)

Algorithmic aspects of type-based program sythesis. - Andrej Dudenhefner (2019)

Undecidability of Semi-Unification on a Napkin. - Andrej Dudenhefner (FSCD, 2020)

The Undecidability of System F Typability and Type Checking for Reductionists. - Andrej Dudenhefner (LICS, 2021)

Kripke Semantics for Intersection Formulas. - Andrej Dudenhefner; Pawel Urzyczyn (ACM Trans. Comput. Log., 2021)

Constructive Many-One Reduction from the Halting Problem to Semi-Unification. - Andrej Dudenhefner (CSL, 2022)

Certified Decision Procedures for Two-Counter Machines. - Andrej Dudenhefner (FSCD, 2022)

Undecidability of Dyadic First-Order Logic in Coq. - Johannes Hostert; Andrej Dudenhefner; Dominik Kirst (ITP, 2022)

Finite Combinatory Logic with Predicates. - Andrej Dudenhefner; Christoph Stahl; Constantin Chaumet; Felix Laarmann; Jakob Rehof (TYPES, 2023)

Constructive Many-one Reduction from the Halting Problem to Semi-unification (Extended Version). - Andrej Dudenhefner (Log. Methods Comput. Sci., 2023)

Mechanized Subject Expansion in Uniform Intersection Types for Perpetual Reductions. - Andrej Dudenhefner; Daniele Pautasso (FSCD, 2024)

Mechanized Undecidability of Higher-Order Beta-Matching. - Andrej Dudenhefner (FSCD, 2025)