Ambrus Kaposi

ORCID

Publication Activity (10 Years)

Years Active: 2014-2024
Publications (10 Years): 27

Top Venues

CoRR

FSCD

TYPES

Proc. ACM Program. Lang.

University of Nottingham, UK (PHD)

Education History

University of Nottingham, UK

PHD

Publications

Ambrus Kaposi, Szumi Xie
Second-Order Generalised Algebraic Theories: Signatures and First-Order Semantics. FSCD (2024)
Thorsten Altenkirch, Yorgo Chamoun, Ambrus Kaposi, Michael Shulman
Internal Parametricity, without an Interval. Proc. ACM Program. Lang. 8 (POPL) (2024)
Thorsten Altenkirch, Ambrus Kaposi, Artjoms Sinkarovs, Tamás Végh
Combinatory Logic and Lambda Calculus Are Equal, Algebraically. FSCD (2023)
Rafaël Bocquet, Ambrus Kaposi, Christian Sattler
For the Metatheory of Type Theory, Internal Sconing Is Enough. FSCD (2023)
Thorsten Altenkirch, Yorgo Chamoun, Ambrus Kaposi, Michael Shulman
Internal parametricity, without an interval. CoRR (2023)
Rafaël Bocquet, Ambrus Kaposi, Christian Sattler
For the Metatheory of Type Theory, Internal Sconing Is Enough. CoRR (2023)
Thorsten Altenkirch, Ambrus Kaposi, Artjoms Sinkarovs, Tamás Végh
The Münchhausen Method in Type Theory. TYPES (2022)
Rafaël Bocquet, Ambrus Kaposi, Christian Sattler
Induction principles for type theories, internally to presheaf categories. CoRR (2021)
István Donkó, Ambrus Kaposi
Internal Strict Propositions Using Point-Free Equations. TYPES (2021)
Thorsten Altenkirch, Simon Boulier, Ambrus Kaposi, Christian Sattler, Filippo Sestini
Constructing a universe for the setoid model. FoSSaCS (2021)
Ambrus Kaposi, Jakob von Raumer
A Syntax for Mutual Inductive Families. FSCD (2020)
András Kovács, Ambrus Kaposi
Large and Infinitary Quotient Inductive-Inductive Types. CoRR (2020)
Ambrus Kaposi, András Kovács
Signatures and Induction Principles for Higher Inductive-Inductive Types. Log. Methods Comput. Sci. 16 (1) (2020)
András Kovács, Ambrus Kaposi
Large and Infinitary Quotient Inductive-Inductive Types. LICS (2020)
Ambrus Kaposi, András Kovács
Signatures and Induction Principles for Higher Inductive-Inductive Types. CoRR (2019)
Ambrus Kaposi, András Kovács, Thorsten Altenkirch
Constructing quotient inductive-inductive types. Proc. ACM Program. Lang. 3 (POPL) (2019)
Ambrus Kaposi, András Kovács, Nicolai Kraus
Shallow Embedding of Type Theory is Morally Correct. CoRR (2019)
Ambrus Kaposi, András Kovács, Ambroise Lafont
For Finitary Induction-Induction, Induction Is Enough. TYPES (2019)
Ambrus Kaposi, Simon Huber, Christian Sattler
Gluing for Type Theory. FSCD (2019)
Thorsten Altenkirch, Simon Boulier, Ambrus Kaposi, Nicolas Tabareau
Setoid Type Theory - A Syntactic Translation. MPC (2019)
Ambrus Kaposi, András Kovács, Nicolai Kraus
Shallow Embedding of Type Theory is Morally Correct. MPC (2019)
Ambrus Kaposi, András Kovács
A Syntax for Higher Inductive-Inductive Types. FSCD (2018)
Thorsten Altenkirch, Ambrus Kaposi
Normalisation by Evaluation for Type Theory, in Type Theory. Log. Methods Comput. Sci. 13 (4) (2017)
Thorsten Altenkirch, Ambrus Kaposi
Type theory in type theory using quotient inductive types. POPL (2016)
Thorsten Altenkirch, Ambrus Kaposi
Normalisation by Evaluation for Type Theory, in Type Theory. CoRR (2016)
Thorsten Altenkirch, Ambrus Kaposi
Normalisation by Evaluation for Dependent Types. FSCD (2016)
Thorsten Altenkirch, Ambrus Kaposi
Towards a Cubical Type Theory without an Interval. TYPES (2015)
Paolo Capriotti, Ambrus Kaposi
Free Applicative Functors. MSFP (2014)

Ambrus Kaposi.css-eqlu8i{font-size:small;padding-left:4px;}

Publication Activity (10 Years)

Top Topics

Top Venues

Ambrus Kaposi