Ambrus Kaposi

According to our database, Ambrus Kaposi authored at least 22 papers between 2014 and 2024.

Collaborative distances:

• Dijkstra number of five.
• Erdős number of four.

2024

Internal Parametricity, without an Interval.

Thorsten Altenkirch, Yorgo Chamoun, Ambrus Kaposi, Michael Shulman

Proc. ACM Program. Lang., January, 2024

2023

For the Metatheory of Type Theory, Internal Sconing Is Enough.

Rafaël Bocquet, Ambrus Kaposi, Christian Sattler

Proceedings of the 8th International Conference on Formal Structures for Computation and Deduction, 2023

Combinatory Logic and Lambda Calculus Are Equal, Algebraically.

Thorsten Altenkirch, Ambrus Kaposi, Artjoms Sinkarovs, Tamás Végh

Proceedings of the 8th International Conference on Formal Structures for Computation and Deduction, 2023

2022

The Münchhausen Method in Type Theory.

Thorsten Altenkirch, Ambrus Kaposi, Artjoms Sinkarovs, Tamás Végh

Proceedings of the 28th International Conference on Types for Proofs and Programs, 2022

2021

Induction principles for type theories, internally to presheaf categories.

Rafaël Bocquet, Ambrus Kaposi, Christian Sattler

CoRR, 2021

Internal Strict Propositions Using Point-Free Equations.

István Donkó, Ambrus Kaposi

Proceedings of the 27th International Conference on Types for Proofs and Programs, 2021

Constructing a universe for the setoid model.

Thorsten Altenkirch, Simon Boulier, Ambrus Kaposi, Christian Sattler, Filippo Sestini

Proceedings of the Foundations of Software Science and Computation Structures, 2021

2020

Signatures and Induction Principles for Higher Inductive-Inductive Types.

Ambrus Kaposi, András Kovács

Log. Methods Comput. Sci., 2020

Large and Infinitary Quotient Inductive-Inductive Types.

András Kovács, Ambrus Kaposi

Proceedings of the LICS '20: 35th Annual ACM/IEEE Symposium on Logic in Computer Science, 2020

A Syntax for Mutual Inductive Families.

Ambrus Kaposi, Jakob von Raumer

Proceedings of the 5th International Conference on Formal Structures for Computation and Deduction, 2020

2019

Constructing quotient inductive-inductive types.

Ambrus Kaposi, András Kovács, Thorsten Altenkirch

Proc. ACM Program. Lang., 2019

For Finitary Induction-Induction, Induction Is Enough.

Ambrus Kaposi, András Kovács, Ambroise Lafont

Proceedings of the 25th International Conference on Types for Proofs and Programs, 2019

Gluing for Type Theory.

Ambrus Kaposi, Simon Huber, Christian Sattler

Proceedings of the 4th International Conference on Formal Structures for Computation and Deduction, 2019

Shallow Embedding of Type Theory is Morally Correct.

Ambrus Kaposi, András Kovács, Nicolai Kraus

Proceedings of the Mathematics of Program Construction - 13th International Conference, 2019

Setoid Type Theory - A Syntactic Translation.

Thorsten Altenkirch, Simon Boulier, Ambrus Kaposi, Nicolas Tabareau

Proceedings of the Mathematics of Program Construction - 13th International Conference, 2019

2018

A Syntax for Higher Inductive-Inductive Types.

Ambrus Kaposi, András Kovács

Proceedings of the 3rd International Conference on Formal Structures for Computation and Deduction, 2018

2017

Type theory in a type theory with quotient inductive types.

Ambrus Kaposi

PhD thesis, 2017

Normalisation by Evaluation for Type Theory, in Type Theory.

Thorsten Altenkirch, Ambrus Kaposi

Log. Methods Comput. Sci., 2017

2016

Normalisation by Evaluation for Dependent Types.

Thorsten Altenkirch, Ambrus Kaposi

Proceedings of the 1st International Conference on Formal Structures for Computation and Deduction, 2016

Type theory in type theory using quotient inductive types.

Thorsten Altenkirch, Ambrus Kaposi

Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2016

2015

Towards a Cubical Type Theory without an Interval.

Thorsten Altenkirch, Ambrus Kaposi

Proceedings of the 21st International Conference on Types for Proofs and Programs, 2015

2014

Free Applicative Functors.

Paolo Capriotti, Ambrus Kaposi

Proceedings of the Proceedings 5th Workshop on Mathematically Structured Functional Programming, 2014