| 2026 | CSL | The Groupoid-Syntax of Type Theory Is a Set. | Thorsten Altenkirch, Ambrus Kaposi, Szumi Xie |
| 2024 | FSCD | Second-Order Generalised Algebraic Theories: Signatures and First-Order Semantics. | Ambrus Kaposi, Szumi Xie |
| 2023 | FSCD | Combinatory Logic and Lambda Calculus Are Equal, Algebraically. | Thorsten Altenkirch, Ambrus Kaposi, Artjoms Sinkarovs, Tams Vgh |
| 2023 | FSCD | For the Metatheory of Type Theory, Internal Sconing Is Enough. | Rafal Bocquet, Ambrus Kaposi, Christian Sattler |
| 2021 | FOSSACS | Constructing a universe for the setoid model. | Thorsten Altenkirch, Simon Boulier, Ambrus Kaposi, Christian Sattler, Filippo Sestini |
| 2020 | FSCD | A Syntax for Mutual Inductive Families. | Ambrus Kaposi, Jakob von Raumer |
| 2020 | LICS | Large and Infinitary Quotient Inductive-Inductive Types. | Andrs Kovcs, Ambrus Kaposi |
| 2019 | MPC | Setoid Type Theory - A Syntactic Translation. | Thorsten Altenkirch, Simon Boulier, Ambrus Kaposi, Nicolas Tabareau |
| 2019 | MPC | Shallow Embedding of Type Theory is Morally Correct. | Ambrus Kaposi, Andrs Kovcs, Nicolai Kraus |
| 2016 | POPL | Type theory in type theory using quotient inductive types. | Thorsten Altenkirch, Ambrus Kaposi |