Type Theory Research Group

2025.03.31.

About us

We are developing new programming languages with dependent types and study the metatheory of such languages. For example, we study the different classes of inductive types, high level descriptions of programming languages as initial models of algebraic theories, extensional principles in type theory, homotopy type theory, strictness in type theory, efficient implementations of type checkers.

Group's own website: external link

Research interests

▶ Metatheory of Martin-Löf’s type theory

alternatív szöveg — ➥ *Programs in a functional programming language at different levels of abstraction.* At each of the six levels of abstraction, a bubble represents a program. At level (1) a program is a string, this is the most concrete level, at level (6) a program is a well-typed syntax tree quotiented by conversion, this is the most abstract level.

▶ Extensions of type theory with extensionality, univalence, parametricity, new definitional equalities

➥ *Illustration of representing an infinite-dimensional structure (above) by a finite diagram (left, below), and a syntax of a language coming directly from the finite diagram (right, below).*

▶ Formalisation of mathematics in proof assistants

▶ Implementation of dependently typed programming languages and proof assistants

Research methodology

The theoretical methods from the theory of programming languages and category theory, the proof assistants Agda and Coq are used. New softwares in Haskell and OCaml are developed..

Research staff

Viktor Bense PhD student
Rafaël Bocquet PhD student
Viktor Csimma BSc student
Ambrus Kaposi associate professor
Péter Zsolt Korpa MSc student
Márton Petes MSc student
Bálint Bence Török BSc student
Szumi Xie PhD student
Zhenyun Yin BSc student

Grants awarded

Higher Observational Type Theory (HOTT) ERC Consolidator Grant
COST action EuroProofNet CA20111
„Application Domain Specific Highly Reliable IT Solutions” project of the Thematic Excellence Programme TKP2020-NKA-06 (National Challenges Subprogramme) funding scheme
COST Action EUTypes CA15123
EFOP-3.6.3-VEKOP-16-2017-00002

5 important publications in the field

Thorsten Altenkirch, Yorgo Chamoun, Ambrus Kaposi, Michael Shulman: Internal Parametricity, without an Interval. Proc. ACM Program. Lang. 8(POPL): 2340-2369 (2024) https://doi.org/10.1145/3632920
Rafaël Bocquet, Ambrus Kaposi, Christian Sattler: For the Metatheory of Type Theory, Internal Sconing Is Enough. FSCD 2023: 18:1-18:23 https://doi.or/10.4230/LIPIcs.FSCD.2023.18
András Kovács: Staged compilation with two-level type theory. Proc. ACM Program. Lang. 6(ICFP): 540-569 (2022) https://doi.org/10.1145/3547641
Ambrus Kaposi, András Kovács: Signatures and Induction Principles for Higher Inductive-Inductive Types. Log. Methods Comput. Sci. 16(1) (2020) https://doi.org/10.23638/LMCS-16(1:10)2020
Ambrus Kaposi, András Kovács, Thorsten Altenkirch: Constructing quotient inductive-inductive types. Proc. ACM Program. Lang. 3(POPL): 2:1-2:24 (2019) https://doi.org/10.1145/3290315

Contact

Ambrus Kaposi associate professor: akaposi@inf.elte.hu