Ambrus Kaposi

35 papers A* 2B 11Journal 14Unranked 6
YearRankTypeTitle / Venue / Authors
2026 J jnl
For Generalised Algebraic Theories, Two Sorts Are Enough.
CoRR
Samy Avrillon, Ambrus Kaposi, Ambroise Lafont, Niyousha Najmaei, Johann Rosain
2026 B conf
The Groupoid-Syntax of Type Theory Is a Set.
CSL
Thorsten Altenkirch, Ambrus Kaposi, Szumi Xie
2025 J jnl
The Groupoid-syntax of Type Theory is a Set.
CoRR
Thorsten Altenkirch, Ambrus Kaposi, Szumi Xie
2025 J jnl
Type Theory in Type Theory using a Strictified Syntax.
Proc. ACM Program. Lang.
Ambrus Kaposi, Loïc Pujet
2025 — conf
Type Theory with Single Substitutions.
LFMTP@FSCD
Ambrus Kaposi, Szumi Xie
2024 J jnl
Internal Parametricity, without an Interval.
Proc. ACM Program. Lang.
Thorsten Altenkirch, Yorgo Chamoun, Ambrus Kaposi, Michael Shulman
2024 B conf
Second-Order Generalised Algebraic Theories: Signatures and First-Order Semantics.
FSCD
Ambrus Kaposi, Szumi Xie
2023 B conf
Combinatory Logic and Lambda Calculus Are Equal, Algebraically.
FSCD
Thorsten Altenkirch, Ambrus Kaposi, Artjoms Sinkarovs, Tamás Végh
2023 B conf
For the Metatheory of Type Theory, Internal Sconing Is Enough.
FSCD
Rafaël Bocquet, Ambrus Kaposi, Christian Sattler
2023 J jnl
For the Metatheory of Type Theory, Internal Sconing Is Enough.
CoRR
Rafaël Bocquet, Ambrus Kaposi, Christian Sattler
2023 J jnl
Internal parametricity, without an interval.
CoRR
Thorsten Altenkirch, Yorgo Chamoun, Ambrus Kaposi, Michael Shulman
2022 — conf
The Münchhausen Method in Type Theory.
TYPES
Thorsten Altenkirch, Ambrus Kaposi, Artjoms Sinkarovs, Tamás Végh
2021 B conf
Constructing a universe for the setoid model.
FoSSaCS
Thorsten Altenkirch, Simon Boulier, Ambrus Kaposi, Christian Sattler, Filippo Sestini
2021 J jnl
Induction principles for type theories, internally to presheaf categories.
CoRR
Rafaël Bocquet, Ambrus Kaposi, Christian Sattler
2021 — conf
Internal Strict Propositions Using Point-Free Equations.
TYPES
István Donkó, Ambrus Kaposi
2020 B conf
A Syntax for Mutual Inductive Families.
FSCD
Ambrus Kaposi, Jakob von Raumer
2020 A* conf
Large and Infinitary Quotient Inductive-Inductive Types.
LICS
András Kovács, Ambrus Kaposi
2020 J jnl
Large and Infinitary Quotient Inductive-Inductive Types.
CoRR
András Kovács, Ambrus Kaposi
2020 J jnl
Signatures and Induction Principles for Higher Inductive-Inductive Types.
Log. Methods Comput. Sci.
Ambrus Kaposi, András Kovács
2019 J jnl
Constructing quotient inductive-inductive types.
Proc. ACM Program. Lang.
Ambrus Kaposi, András Kovács, Thorsten Altenkirch
2019 — conf
For Finitary Induction-Induction, Induction Is Enough.
TYPES
Ambrus Kaposi, András Kovács, Ambroise Lafont
2019 B conf
Gluing for Type Theory.
FSCD
Ambrus Kaposi, Simon Huber, Christian Sattler
2019 B conf
Setoid Type Theory - A Syntactic Translation.
MPC
Thorsten Altenkirch, Simon Boulier, Ambrus Kaposi, Nicolas Tabareau
2019 B conf
Shallow Embedding of Type Theory is Morally Correct.
MPC
Ambrus Kaposi, András Kovács, Nicolai Kraus
2019 J jnl
Shallow Embedding of Type Theory is Morally Correct.
CoRR
Ambrus Kaposi, András Kovács, Nicolai Kraus
2019 J jnl
Signatures and Induction Principles for Higher Inductive-Inductive Types.
CoRR
Ambrus Kaposi, András Kovács
2018 — ed.
23rd International Conference on Types for Proofs and Programs, TYPES 2017, Budapest, Hungary, May 29 - June 1, 2017
TYPES
Andreas Abel, Fredrik Nordvall Forsberg, Ambrus Kaposi
2018 B conf
A Syntax for Higher Inductive-Inductive Types.
FSCD
Ambrus Kaposi, András Kovács
2017 J jnl
Normalisation by Evaluation for Type Theory, in Type Theory.
Log. Methods Comput. Sci.
Thorsten Altenkirch, Ambrus Kaposi
2017 — —
Type theory in a type theory with quotient inductive types.
Ambrus Kaposi
2016 B conf
Normalisation by Evaluation for Dependent Types.
FSCD
Thorsten Altenkirch, Ambrus Kaposi
2016 J jnl
Normalisation by Evaluation for Type Theory, in Type Theory.
CoRR
Thorsten Altenkirch, Ambrus Kaposi
2016 A* conf
Type theory in type theory using quotient inductive types.
POPL
Thorsten Altenkirch, Ambrus Kaposi
2015 — conf
Towards a Cubical Type Theory without an Interval.
TYPES
Thorsten Altenkirch, Ambrus Kaposi
2014 — conf
Free Applicative Functors.
MSFP
Paolo Capriotti, Ambrus Kaposi