Free Applicative Functors. - Paolo Capriotti; Ambrus Kaposi (MSFP, 2014)

Towards a Cubical Type Theory without an Interval. - Thorsten Altenkirch; Ambrus Kaposi (TYPES, 2015)

Type theory in type theory using quotient inductive types. - Thorsten Altenkirch; Ambrus Kaposi (POPL, 2016)

Normalisation by Evaluation for Dependent Types. - Thorsten Altenkirch; Ambrus Kaposi (FSCD, 2016)

Normalisation by Evaluation for Type Theory, in Type Theory. - Thorsten Altenkirch; Ambrus Kaposi (Log. Methods Comput. Sci., 2017)

Type theory in a type theory with quotient inductive types. - Ambrus Kaposi (2017)

A Syntax for Higher Inductive-Inductive Types. - Ambrus Kaposi; András Kovács (FSCD, 2018)

Setoid Type Theory - A Syntactic Translation. - Thorsten Altenkirch; Simon Boulier; Ambrus Kaposi; Nicolas Tabareau (MPC, 2019)

Shallow Embedding of Type Theory is Morally Correct. - Ambrus Kaposi; András Kovács; Nicolai Kraus (MPC, 2019)

Gluing for Type Theory. - Ambrus Kaposi; Simon Huber; Christian Sattler (FSCD, 2019)

For Finitary Induction-Induction, Induction Is Enough. - Ambrus Kaposi; András Kovács; Ambroise Lafont (TYPES, 2019)

Constructing quotient inductive-inductive types. - Ambrus Kaposi; András Kovács; Thorsten Altenkirch (Proc. ACM Program. Lang., 2019)

A Syntax for Mutual Inductive Families. - Ambrus Kaposi; Jakob von Raumer (FSCD, 2020)

Large and Infinitary Quotient Inductive-Inductive Types. - András Kovács; Ambrus Kaposi (LICS, 2020)

Signatures and Induction Principles for Higher Inductive-Inductive Types. - Ambrus Kaposi; András Kovács (Log. Methods Comput. Sci., 2020)

Constructing a universe for the setoid model. - Thorsten Altenkirch; Simon Boulier; Ambrus Kaposi; Christian Sattler; Filippo Sestini (FoSSaCS, 2021)

Internal Strict Propositions Using Point-Free Equations. - István Donkó; Ambrus Kaposi (TYPES, 2021)

Induction principles for type theories, internally to presheaf categories. - Rafaël Bocquet; Ambrus Kaposi; Christian Sattler (CoRR, 2021)

The Münchhausen Method in Type Theory. - Thorsten Altenkirch; Ambrus Kaposi; Artjoms Sinkarovs; Tamás Végh (TYPES, 2022)

Combinatory Logic and Lambda Calculus Are Equal, Algebraically. - Thorsten Altenkirch; Ambrus Kaposi; Artjoms Sinkarovs; Tamás Végh (FSCD, 2023)

For the Metatheory of Type Theory, Internal Sconing Is Enough. - Rafaël Bocquet; Ambrus Kaposi; Christian Sattler (FSCD, 2023)

Second-Order Generalised Algebraic Theories: Signatures and First-Order Semantics. - Ambrus Kaposi; Szumi Xie (FSCD, 2024)

Internal Parametricity, without an Interval. - Thorsten Altenkirch; Yorgo Chamoun; Ambrus Kaposi; Michael Shulman (Proc. ACM Program. Lang., 2024)